Theorems · Inductive type · group theory
SubtractionCommMonoid
Type u → Type u
Commutative SubtractionMonoid.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 79 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by95
Results whose statement or proof uses this declaration.
- Finset.sum_sub_distribstatement and proof · cited by 84
- neg_addstatement and proof · cited by 69
- Finset.sum_neg_distribstatement and proof · cited by 65
- sub_substatement and proof · cited by 54
- sub_addstatement and proof · cited by 51
- sub_eq_neg_addstatement and proof · cited by 51
- neg_add_eq_substatement and proof · cited by 33
- sub_add_eq_add_substatement and proof · cited by 29
- add_sub_add_commstatement and proof · cited by 28
- neg_add'statement and proof · cited by 20
- sub_right_commstatement and proof · cited by 15
- zsmulAddGroupHomstatement and proof · cited by 13