Commit 2024-11-21 10:01 c2fcf775

View on Github →

chore: rename Nat.prime_def_lt'' to Nat.prime_def (#19255) Rename the statement Prime p ↔ 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p to Nat.prime_def.

Estimated changes

Modified Mathlib/Algebra/CharP/Defs.lean

Modified Mathlib/Data/Nat/Prime/Defs.lean

added theorem Nat.prime_def

deleted theorem Nat.prime_def_lt''

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/NumberTheory/Divisors.lean

Modified Mathlib/NumberTheory/Fermat.lean

Modified scripts/no_lints_prime_decls.txt