Theorems · Theorem · group theory

IsAddUnit.eq_on_neg

∀ {F : Type u_1} {G : Type u_2} {N : Type u_3} [inst : SubtractionMonoid G] [inst_1 : AddMonoid N]
  [inst_2 : FunLike F G N] [AddMonoidHomClass F G N] {x : G}, IsAddUnit x → ∀ (f g : F), f x = g x → f (-x) = g (-x)

If two homomorphisms from a subtraction monoid to an additive monoid are equal at an additive unit x, then they are equal at -x.

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

1 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext

Assumes

SubtractionMonoidAddMonoidFunLikeAddMonoidHomClass