Theorem multiplicity.finite_prime_left

Modification history

2024-12-06 14:50
Mathlib/Algebra/Squarefree/Basic.lean
chore: eliminate `multiplicity` namespace (#19623)
Deleted multiplicity.finite_prime_leftView on Github →
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_leftView on Github →
2023-03-21 21:27
Mathlib/Algebra/Squarefree.lean
feat: port Algebra.Squarefree (#3018)
Added multiplicity.finite_prime_leftView on Github →