Theorems · Theorem · group theory

eq_on_neg

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

If two homomorphism from an additive group to an additive monoid are equal at x, then they are equal at -x.

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

AddGroupAddMonoidFunLikeAddMonoidHomClass