Theorem Nat.factors_eq

Modification history

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