Theorem IsPrimePow.factorization_minFac_ne_zero

Modification history

2026-02-15 14:33
Mathlib/Data/Nat/Factorization/PrimePow.lean
chore: remove declarations deprecated between 2021-02-15 and 2025-08-15 (#35335) …
Deleted IsPrimePow.factorization_minFac_ne_zeroView on Github →
2024-11-21 17:01
Mathlib/Data/Nat/Factorization/PrimePow.lean
feat(Data/Nat/Factorization/PrimePow): add equivalence Primes × ℕ ≃ PrimePowers (#19335) …
Added IsPrimePow.factorization_minFac_ne_zeroView on Github →