Theorems · Theorem · group theory

map_nsmul

∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : AddMonoid G] [inst_2 : AddMonoid H]
  [AddMonoidHomClass F G H] (f : F) (n : ℕ) (a : G), f (n • a) = n • f a

Defined in

Mathlib.Algebra.Group.Hom.Defs

Cited by

41 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

FunLikeAddMonoidAddMonoidAddMonoidHomClass