Commit 2024-05-11 17:10 83018cff

View on Github →

chore: Move UFD instance for Nat (#12401) This reduces the imports to RingTheory.Int.Basic. Maybe those instances could go to a new file RingTheory.UniqueFactorizationDomain.Nat to avoid having to import Data.Nat.Factors in RingTheory.UniqueFactorizationDomain, but also that new import is much more lightweight than the existing ones.

Estimated changes

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Data/ZMod/Coprime.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

Modified Mathlib/NumberTheory/FLT/Basic.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

Modified Mathlib/RingTheory/Int/Basic.lean

deleted theorem Nat.factors_eq

deleted theorem Nat.factors_multiset_prod_of_irreducible

deleted theorem induction_on_primes

Modified Mathlib/RingTheory/UniqueFactorizationDomain.lean

added theorem Nat.factors_eq

added theorem Nat.factors_multiset_prod_of_irreducible

added theorem induction_on_primes