Theorem Associates.quot_out
Modification history
2026-09-03 14:21
Mathlib/Algebra/GroupWithZero/Associated.lean
fix(Algebra/GroupWithZero/Associated): de-`abbrev` `Associates` (#42394) …
Modified Associates.quot_outView on Github →2024-09-30 02:32
Mathlib/Algebra/Associated/Basic.lean
chore(Associated): use `M`, `N` for type variables (#17115) …
Modified Associates.quot_outView on Github →2023-12-04 11:39
Mathlib/Algebra/Associated.lean
chore: move Associates.quot_out earlier (#8484) …
Modified Associates.quot_outView on Github →