Mathlib Changelog
v4
Changelog
About
Github
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