Theorems · Theorem · group theory

AddConstMapClass.map_add_zsmul

∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddGroup G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (x : G) (n : ℤ), f (x + n • a) = f x + n • b

Defined in

Mathlib.Algebra.AddConstMap.Basic

Cited by

5 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

FunLikeAddGroupAddGroupAddConstMapClass