Theorems · Theorem · group theory
map_neg
∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddGroup G]
[inst_2 : SubtractionMonoid H] [AddMonoidHomClass F G H] (f : F) (a : G), f (-a) = -f aAdditive group homomorphisms preserve negation.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 378 results in Mathlib
- Foundations
- Depth 9 from the axioms, rests on 45 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- AddGroupstatement and proof · cited by 4,410
- FunLikestatement and proof · cited by 2,560
- neg_add_cancelproof · cited by 256
- AddMonoidHomClassstatement and proof · cited by 252
- SubtractionMonoidstatement and proof · cited by 208
- eq_neg_of_add_eq_zero_leftproof · cited by 21
- map_add_eq_zeroproof · cited by 5
Cited by378
Results whose statement or proof uses this declaration.
- map_subproof · cited by 565
- inner_neg_rightproof · cited by 41
- inner_neg_leftproof · cited by 33
- CategoryTheory.Preadditive.comp_negproof · cited by 32
- CategoryTheory.Preadditive.neg_compproof · cited by 31
- Polynomial.C_negproof · cited by 25
- AddMonoidHom.map_negproof · cited by 22
- map_zsmulproof · cited by 18
- Polynomial.X_pow_sub_C_ne_zeroproof · cited by 15
- Polynomial.degree_X_pow_sub_Cproof · cited by 14
- Polynomial.monic_X_pow_sub_Cproof · cited by 13
- Polynomial.leadingCoeff_X_sub_Cproof · cited by 11
Showing the 200 most cited of 378.