Theorems · Theorem · group theory
map_zsmul
∀ {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) (n : ℤ) (g : G), f (n • g) = n • f gAdditive group homomorphisms preserve integer scaling.
- Defined in
- Mathlib.Algebra.Group.Hom.Defs
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- map_negproof · cited by 378
- AddMonoidHomClassstatement and proof · cited by 252
- SubtractionMonoidstatement and proof · cited by 208
- map_zsmul'proof · cited by 4
Cited by18
Results whose statement or proof uses this declaration.
- AddMonoidHom.map_zsmulproof · cited by 10
- CategoryTheory.Preadditive.comp_zsmulproof · cited by 5
- isAddCyclic_of_surjectiveproof · cited by 5
- map_zsmul_unitproof · cited by 4
- RootPairing.Base.IsPos.exists_mem_support_pos_pairingInproof · cited by 3
- map_intCast_smulproof · cited by 3
- IsUnit.isQuotientMap_zsmulproof · cited by 2
- CategoryTheory.Preadditive.zsmul_compproof · cited by 2
- AddMonoidHom.eq_iff_eq_on_generatorproof · cited by 1
- CategoryTheory.Idempotents.Karoubi.zsmul_homproof · cited by 1
- FreeAbelianGroup.support_zsmulproof · cited by 1
- Module.Baer.of_divisibleproof · cited by 1