Commit 2024-06-09 22:38 75349a6d

View on Github →

chore: move NormalizedGCDMonoid ℤ to reduce imports (#12364)

Estimated changes

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Modified Mathlib/Algebra/GCDMonoid/Nat.lean

added theorem Int.abs_eq_normalize

added theorem Int.associated_iff

added theorem Int.associated_iff_natAbs

added theorem Int.associated_natAbs

added theorem Int.coe_gcd

added theorem Int.coe_lcm

added theorem Int.eq_of_associated_of_nonneg

added theorem Int.exists_unit_of_abs

added theorem Int.gcd_eq_natAbs

added theorem Int.natAbs_gcd

added theorem Int.natAbs_lcm

added theorem Int.nonneg_iff_normalize_eq_self

added theorem Int.nonneg_of_normalize_eq_self

added theorem Int.normUnit_eq

added theorem Int.normalize_coe_nat

added theorem Int.normalize_of_nonneg

added theorem Int.normalize_of_nonpos

added def associatesIntEquivNat

Modified Mathlib/NumberTheory/FLT/Basic.lean

Modified Mathlib/NumberTheory/FLT/Three.lean

Modified Mathlib/RingTheory/Int/Basic.lean

deleted theorem Int.abs_eq_normalize

deleted theorem Int.associated_iff

deleted theorem Int.associated_iff_natAbs

deleted theorem Int.associated_natAbs

deleted theorem Int.coe_gcd

deleted theorem Int.coe_lcm

deleted theorem Int.eq_of_associated_of_nonneg

deleted theorem Int.exists_unit_of_abs

deleted theorem Int.gcd_eq_natAbs

deleted theorem Int.natAbs_gcd

deleted theorem Int.natAbs_lcm

deleted theorem Int.nonneg_iff_normalize_eq_self

deleted theorem Int.nonneg_of_normalize_eq_self

deleted theorem Int.normUnit_eq

deleted theorem Int.normalize_coe_nat

deleted theorem Int.normalize_of_nonneg

deleted theorem Int.normalize_of_nonpos

deleted def associatesIntEquivNat