Commit 2023-06-16 18:02 3de751e5

View on Github →

feat: port NumberTheory.PrimesCongruentOne (#5146)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/PrimesCongruentOne.lean

added theorem Nat.exists_prime_gt_modEq_one

added theorem Nat.frequently_atTop_modEq_one

added theorem Nat.infinite_setOf_prime_modEq_one