Commit 2025-07-05 07:48 9a3e26ec

View on Github →

chore(Data/Nat/Factorization/Basic): minimize dependencies (#24330)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Antidiag/Nat.lean

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

deleted theorem Nat.coprime_factorizationLCMLeft_factorizationLCMRight

deleted theorem Nat.factorizationLCMLeft_dvd_left

deleted theorem Nat.factorizationLCMLeft_mul_factorizationLCMRight

deleted theorem Nat.factorizationLCMLeft_pos

deleted theorem Nat.factorizationLCMLeft_zero_left

deleted theorem Nat.factorizationLCMLeft_zero_right

deleted theorem Nat.factorizationLCMRight_dvd_right

deleted theorem Nat.factorizationLCMRight_pos

deleted theorem Nat.factorizationLCMRight_zero_right

deleted theorem Nat.factorizationLCRight_zero_left

deleted theorem Nat.factorization_one_right

deleted theorem Nat.ordProj_dvd_ordProj_iff_dvd

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

added theorem Nat.factorization_one_right

added theorem Nat.ordProj_dvd_ordProj_iff_dvd

Created Mathlib/Data/Nat/Factorization/LCM.lean

added theorem Nat.coprime_factorizationLCMLeft_factorizationLCMRight

added theorem Nat.factorizationLCMLeft_dvd_left

added theorem Nat.factorizationLCMLeft_mul_factorizationLCMRight

added theorem Nat.factorizationLCMLeft_pos

added theorem Nat.factorizationLCMLeft_zero_left

added theorem Nat.factorizationLCMLeft_zero_right

added theorem Nat.factorizationLCMRight_dvd_right

added theorem Nat.factorizationLCMRight_pos

added theorem Nat.factorizationLCMRight_zero_right

added theorem Nat.factorizationLCRight_zero_left

Modified Mathlib/GroupTheory/Exponent.lean

Modified Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean