Theorems · Theorem · group theory
sub_eq_add_neg
∀ {G : Type u_1} [inst : SubNegMonoid G] (a b : G), a - b = a + -bSubtracting an element is the same as adding by its negative.
This is a duplicate of SubNegMonoid.sub_eq_add_neg ensuring that the types unfold better.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 1,023 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 35 definitions · uses no axioms
- Assumes
- SubNegMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SubNegMonoidstatement and proof · cited by 79
- SubNegMonoid.sub_eq_add_negproof · cited by 3
Cited by1,023
Results whose statement or proof uses this declaration.
- sub_selfproof · cited by 996
- sub_zeroproof · cited by 938
- sub_add_cancelproof · cited by 344
- neg_subproof · cited by 272
- sub_neg_eq_addproof · cited by 264
- add_sub_cancel_rightproof · cited by 187
- sub_nonnegproof · cited by 167
- sub_posproof · cited by 147
- smul_subproof · cited by 142
- Int.cast_addproof · cited by 124
- sub_smulproof · cited by 97
- Int.cast_subproof · cited by 78
Showing the 200 most cited of 1,023.