Theorem Nat.factorization_eq_zero_of_not_prime

Modification history

2025-10-24 18:46
Mathlib/Data/Nat/Factorization/Defs.lean
chore: deprecate Nat.factorization_eq_zero_of_non_prime (#30862)
Added Nat.factorization_eq_zero_of_not_primeView on Github →