Def Associates

Modification history

2026-09-03 14:21

Mathlib/Algebra/GroupWithZero/Associated.lean

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

Added Associates View on Github →