Theorems · Theorem · group theory

map_comp_neg

∀ {ι : Type u_1} {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) (g : ι → G), ⇑f ∘ (-g) = -⇑f ∘ g

Defined in

Mathlib.Algebra.Group.Hom.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

FunLikeAddGroupSubtractionMonoidAddMonoidHomClass