Theorems · Theorem · group theory
neg_add_rev
∀ {G : Type u_1} [inst : SubtractionMonoid G] (a b : G), -(a + b) = -b + -a- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 236 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 31 definitions · uses no axioms
- Assumes
- SubtractionMonoid
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.
- SubtractionMonoidstatement and proof · cited by 208
- SubtractionMonoid.neg_add_revproof · cited by 1
Cited by236
Results whose statement or proof uses this declaration.
- neg_subproof · cited by 272
- Int.cast_negproof · cited by 224
- Int.cast_addproof · cited by 124
- zsmul_eq_mulproof · cited by 120
- Int.cast_mulproof · cited by 113
- neg_addproof · cited by 69
- sub_subproof · cited by 54
- sub_addproof · cited by 51
- add_sub_add_commproof · cited by 28
- Int.cast_smul_eq_zsmulproof · cited by 28
- zsmul_oneproof · cited by 26
- isUniformAddGroup_of_addCommGroupproof · cited by 21
Showing the 200 most cited of 236.