Def SubNegMonoid.sub'

Modification history

2026-09-18 15:04
Mathlib/Algebra/Group/DivInvMonoid.lean
chore: catch up on a lot of `to_additive` debt (#43814) …
Deleted SubNegMonoid.sub'View on Github →
2026-08-20 19:44
Mathlib/Algebra/Group/Defs.lean
refactor(Algebra/Group): split overlong file Defs.lean (#42952) …
Modified SubNegMonoid.sub'View on Github →
2023-03-07 22:58
Mathlib/Algebra/Group/Defs.lean
chore: don't inline `DivInvMonoid` default value for `Div`, for better instance transparency (#1897) …
Added SubNegMonoid.sub'View on Github →