Commit 2025-01-18 21:34 b10900e7

View on Github →

chore(Associated): split out Ring results (#20737)

Estimated changes

Modified Archive/Imo/Imo2001Q6.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Associated.lean

Modified Mathlib/Algebra/GCDMonoid/Basic.lean

Renamed Mathlib/Algebra/Associated/Basic.lean to Mathlib/Algebra/GroupWithZero/Associated.lean

deleted theorem Associated.neg_left

deleted theorem Associated.neg_neg

deleted theorem Associated.neg_right

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

Modified Mathlib/Algebra/IsPrimePow.lean

Renamed Mathlib/Algebra/Associated/OrderedCommMonoid.lean to Mathlib/Algebra/Order/Monoid/Associated.lean

Modified Mathlib/Algebra/Polynomial/Monic.lean

Created Mathlib/Algebra/Ring/Associated.lean

added theorem Associated.neg_left

added theorem Associated.neg_neg

added theorem Associated.neg_right

Modified Mathlib/Data/Int/Associated.lean

Modified Mathlib/Data/List/Prime.lean

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

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

Modified Mathlib/RingTheory/Ideal/Span.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/Nilpotent/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean

Modified MathlibTest/propose.lean