Theorems · Theorem · group theory

map_inv

∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
  [MonoidHomClass F G H] (f : F) (a : G), f a⁻¹ = (f a)⁻¹

Group homomorphisms preserve inverse. See note [hom simp lemma priority]

Defined in

Mathlib.Algebra.Group.Hom.Defs

Cited by

95 results in Mathlib

Foundations

Depth 9 from the axioms, rests on 45 definitions · uses no axioms

Assumes

FunLikeGroupDivisionMonoidMonoidHomClass