coe_eq_inv_of_involutive — Mathlib

English

Let G be a finite group and let φ be an endomorphism of G that is fixed-point-free and involutive. Then φ acts on G by inversion, i.e., for every g ∈ G, φ(g) = g^{-1}. In particular, φ is the inversion map on G.

Русский

Пусть G — конечная группа и φ: G → G — эндоморфизм, который не имеет ненасыщенных неподвижных точек и удовлетворяет φ^2 = id. Тогда φ совпадает с обращением: для каждого g ∈ G выполняется φ(g) = g^{-1}. В частности, φ равен отображению инверсии на G.

LaTeX

$$$\\forall G\\,[Group\\ G],\\,[Finite\\ G],\\forall \\varphi:\\,G\\to G,\\ FixedPointFree(\\varphi) \\land Involutive(\\varphi) \\Rightarrow \\varphi = (\\cdot)^{-1}$$$

Lean4

theorem coe_eq_inv_of_involutive (hφ : FixedPointFree φ) (h2 : Function.Involutive φ) : ⇑φ = (·⁻¹) :=
  coe_eq_inv_of_sq_eq_one hφ (funext h2)

Похожие утверждения