Theorem Associates.quotient_out

Modification history

2026-09-03 14:21

Mathlib/Algebra/GroupWithZero/Associated.lean

fix(Algebra/GroupWithZero/Associated): de-`abbrev` `Associates` (#42394) …

Added Associates.quotient_out View on Github →