Structures · Algebra
SubtractionCommMonoid
Commutative SubtractionMonoid.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds add_comm
Extends2
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances10
- NonemptyInterval
- DomAddAct
- Interval
- LinearPMap
- Prod
- OrderDual
- Lex
- AddOpposite
- Colex
- Additive
How is a type an instance?
Loading the hierarchy index…
Assumed by97
- Finset.sum_sub_distrib
- neg_add
- Finset.sum_neg_distrib
- sub_sub
- sub_eq_neg_add
- sub_add
- neg_add_eq_sub
- sub_add_eq_add_sub
- add_sub_add_comm
- neg_add'
- sub_right_comm
- neg_sub_neg
- zsmulAddGroupHom
- sub_add_eq_sub_sub
- sub_add_sub_comm
- neg_sub'
- add_sub_right_comm
- AddEquiv.neg
- Function.Periodic.sub_eq'
- Finsupp.sum_sub
- sub_sub_sub_comm
- add_comm_sub
- negAddMonoidHom
- Function.Antiperiodic.sub_eq'
- Finsupp.sum_zsmul
- Multiset.sum_map_sub
- zsmul_sub
- zsmul_add
- finsum_sub_distrib
- sub_sub_sub_eq
- IsAddUnit.sub_eq_sub_iff
- Multiset.sum_map_neg
- Multiset.sum_map_neg'
- zsmulAddGroupHom_apply
- neg_sub_comm
- nsmul_sub
- sub_add_comm
- IsLocalizedModule.mk'_neg
- Even.sub
- AddEquiv.neg_apply
- Multiset.sum_map_zsmul
- add_sub_left_comm
- Flow.reverse
- List.alternatingSum_eq_finsetSum
- finsum_mem_neg_distrib
- finsum_neg_distrib
- List.sum_neg
- negAddMonoidHom_comp_negAddMonoidHom
- coe_negAddMonoidHom
- subAddMonoidHom