coe_eq_inv_of_sq_eq_one — Mathlib

English

If a fixed-point-free endomorphism φ satisfies φ^2 = id, then φ is the inversion map g ↦ g^{-1} for all g ∈ G.

Русский

Если фикс-фри эндоморфизм φ удовлетворяет φ^2 = id, то φ = inv_G, то есть φ(g)=g^{-1} для всех g.

LaTeX

$$$\text{FixedPointFree}(\varphi) \land φ^{2}=\mathrm{id} \Rightarrow \varphi = (\cdot)^{-1}$$$

Lean4

theorem coe_eq_inv_of_sq_eq_one (hφ : FixedPointFree φ) (h2 : φ^[2] = _root_.id) : ⇑φ = (·⁻¹) :=
  by
  ext g
  have key : g * φ g = 1 := by simpa [List.range_succ] using hφ.prod_pow_eq_one h2 g
  rwa [← inv_eq_iff_mul_eq_one, eq_comm] at key

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