Theorem Nat.factors_multiset_prod_of_irreducible

Modification history

2024-11-20 11:43
Mathlib/RingTheory/UniqueFactorizationDomain.lean
chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …
Modified Nat.factors_multiset_prod_of_irreducibleView on Github →
2024-05-11 17:10
Mathlib/RingTheory/Int/Basic.lean
chore: Move UFD instance for `Nat` (#12401) …
Modified Nat.factors_multiset_prod_of_irreducibleView on Github →
2023-03-21 13:00
Mathlib/RingTheory/Int/Basic.lean
feat: port RingTheory.Int.Basic (#3014)
Added Nat.factors_multiset_prod_of_irreducibleView on Github →