stabilizerMulEquiv — Mathlib

English

If g is a three-cycle, then its order is 3.

Русский

Если g — трёхцикл, то его порядок равен 3.

LaTeX

$$orderOf g = 3$$

Lean4

/-- The `MulEquiv` from the `MulOpposite` of `MulAction.stabilizer (Perm α)ᵈᵐᵃ f`
  to the product of the `Equiv.Perm {a // f a = i}` -/
def stabilizerMulEquiv : (stabilizer (Perm α)ᵈᵐᵃ f)ᵐᵒᵖ ≃* (∀ i, Perm { a // f a = i })
    where
  toFun g
    i :=
    Perm.subtypePerm (mk.symm g.unop) fun a ↦ by rw [← Function.comp_apply (f := f), mem_stabilizer_iff.mp g.unop.prop]
  invFun
    g :=
    ⟨mk (stabilizerEquiv_invFun_aux g), by
      ext a
      rw [smul_apply, symm_apply_apply, Perm.smul_def]
      apply comp_stabilizerEquiv_invFun⟩
  right_inv g := by ext i a; apply stabilizerEquiv_invFun_eq
  map_mul' _ _ := rfl

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