Commit 2025-10-24 18:46 afceaae5

View on Github →

chore: deprecate Nat.factorization_eq_zero_of_non_prime (#30862)

Estimated changes

Modified Mathlib/Data/Nat/Choose/Factorization.lean

Modified Mathlib/Data/Nat/Factorization/Basic.lean

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

deleted theorem Nat.factorization_eq_zero_of_non_prime

added theorem Nat.factorization_eq_zero_of_not_prime

Modified Mathlib/Data/Nat/Factorization/PrimePow.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/NumberTheory/Bertrand.lean