Theorems · Theorem · order theory

GroupSeminormClass.map_inv_eq_map

∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Group α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : GroupSeminormClass F α β] (f : F) (a : α), f a⁻¹ = f a

The map is invariant under inversion of its argument.

Defined in

Mathlib.Algebra.Order.Hom.Basic

Cited by

3 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

GroupSeminormClass