Theorem multiplicity.finite_prime_left

Modification history

2024-03-01 06:30

Mathlib/Algebra/Squarefree/Basic.lean

feat(RingTheory/UniqueFactorizationDomain): add `WfDvdMonoid.max_power_factor[']` and `multiplicity.finite_of_not_isUnit` (#11066) …

Modified multiplicity.finite_prime_left View on Github →

2023-03-21 21:27

Mathlib/Algebra/Squarefree.lean

feat: port Algebra.Squarefree (#3018)

Added multiplicity.finite_prime_left View on Github →