Diffusion afp-devel 1ebd4536fe74

New entry Kummer_Congruence
1ebd4536fe74
Actions

Tags

None

Subscribers

None

Description

New entry Kummer_Congruence

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFPceff43a60f39: sitegen for CondNormReasHOL

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFP1ebd4536fe74: New entry Kummer_Congruence.Mar 29 2024, 1:37 PM

Changes (13)

Path

Size

Kummer_Congruence

Irregular_Primes_Infinite.thy

Kummer_Congruence.thy

Kummer_Library.thy

Rat_Congruence.thy

Regular_Primes.thy

Voronoi_Congruence.thy

rAFP1ebd4536fe74

thys/Kummer_Congruence/Irregular_Primes_Infinite.thy

Loading...

thys/Kummer_Congruence/Kummer_Congruence.thy

Loading...

thys/Kummer_Congruence/Kummer_Library.thy

Loading...

thys/Kummer_Congruence/ROOT

Loading...

thys/Kummer_Congruence/Rat_Congruence.thy

Loading...

thys/Kummer_Congruence/Regular_Primes.thy

Loading...

thys/Kummer_Congruence/Voronoi_Congruence.thy

Loading...

thys/Kummer_Congruence/document/root.bib

Loading...

thys/Kummer_Congruence/document/root.tex

Loading...

thys/ROOTS

Loading...