Theorems · Inductive type · group theory
SubtractionMonoid
Type u → Type u
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
- Cited by
- 208 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · 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 by230
Results whose statement or proof uses this declaration.
- map_substatement and proof · cited by 565
- map_negstatement and proof · cited by 378
- neg_substatement and proof · cited by 272
- sub_neg_eq_addstatement and proof · cited by 264
- neg_add_revstatement and proof · cited by 236
- neg_eq_zerostatement and proof · cited by 171
- neg_ne_zerostatement and proof · cited by 70
- sub_ne_zero_of_nestatement and proof · cited by 51
- neg_zsmulstatement and proof · cited by 41
- eq_of_sub_eq_zerostatement and proof · cited by 27
- AddMonoidHom.map_negstatement and proof · cited by 22
- eq_neg_of_add_eq_zero_leftstatement and proof · cited by 21
Showing the 200 most cited of 230.