Theorem UniqueFactorizationMonoid.max_power_factor

Modification history

2025-01-06 10:15
Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
chore: remove >9 month old deprecations (#20505)
Deleted UniqueFactorizationMonoid.max_power_factorView on Github →
2024-11-20 11:43
Mathlib/RingTheory/UniqueFactorizationDomain.lean
chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …
Modified UniqueFactorizationMonoid.max_power_factorView on Github →
2024-03-01 06:30
Mathlib/RingTheory/UniqueFactorizationDomain.lean
feat(RingTheory/UniqueFactorizationDomain): add `WfDvdMonoid.max_power_factor[']` and `multiplicity.finite_of_not_isUnit` (#11066) …
Modified UniqueFactorizationMonoid.max_power_factorView on Github →
2023-05-10 09:29
Mathlib/RingTheory/UniqueFactorizationDomain.lean
feat(RingTheory/UniqueFactorizationDomain) : add lemma `max_power_factor` as in #18830 (#3558) …
Added UniqueFactorizationMonoid.max_power_factorView on Github →