Commit 2026-09-03 14:21 d6386fda

fix(Algebra/GroupWithZero/Associated): de-abbrev Associates (#42394) Associates is an abbrev for Quotient _, but there are many instances defined on it. Some of them create diamonds with general Quotient instances: Inhabited, Unique, and most notably Preorder. While Associates has a Preorder instance that uses the divisibility relation, any monoid with a Preorder will have its ordering lifted to the Quotient. So currently Associates ℕ has two different LE orders defined on it that disagree on 2 ≤ 3. This changes Associates to a def tagged with @[implicit_reducible].