Structures · Algebra
SubtractionMonoid
A SubtractionMonoid is a SubNegMonoid with involutive negation and such that
-(a + b) = -b + -a and a + b = 0 → -a = b.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds neg_neg, neg_add_rev, neg_eq_of_add
Extends2
Extended by3
Forgetful instances
Every SubtractionMonoid is also a
Provided automatically by
Concrete types that are instances8
- Filter.Germ
- DomAddAct
- Prod
- OrderDual
- Lex
- AddOpposite
- Colex
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by234
- map_sub
- map_neg
- neg_sub
- sub_neg_eq_add
- neg_add_rev
- neg_eq_zero
- neg_ne_zero
- sub_ne_zero_of_ne
- neg_zsmul
- eq_of_sub_eq_zero
- AddMonoidHom.map_neg
- eq_neg_of_add_eq_zero_left
- SignType.coe_neg
- neg_nsmul
- AddMonoidHom.map_sub
- map_zsmul
- mul_zsmul'
- zsmul_zero
- IsAddUnit.addUnit'
- sub_add_eq_sub_sub_swap
- AddMonoidHom.map_zsmul
- sub_sub_eq_add_sub
- AddEquiv.map_sub
- AddEquiv.map_neg
- neg_eq_of_add_eq_zero_right
- AddUnits.val_neg_eq_neg_val
- eq_neg_of_add_eq_zero_right
- Function.support_neg
- zsmul_neg
- zsmul_neg'
- zero_eq_neg
- mul_zsmul
- neg_one_zsmul_add
- IsAddUnit.add_neg_cancel
- neg_eq_of_add_eq_zero_left
- Function.support_sub
- IsAddUnit.sub_add_cancel
- even_neg
- Set.add_eq_zero_iff
- map_comp_neg
- IsAddUnit.add_neg_cancel_right
- MeasureTheory.Measure.measurePreserving_sub_left
- IsAddUnit.neg
- ProbabilityTheory.HasIndepIncrements.map'
- AddSemiconjBy.neg_neg_symm_iff
- IsAddUnit.add_neg_cancel_left
- AddEquiv.neg'
- Function.support_fun_neg
- Function.Antiperiodic.add_zsmul_eq
- Function.Antiperiodic.int_mul_eq_of_eq_zero