ofPermHomFun — Mathlib

English

For any Basis a and x ∈ α, either x is fixed by g or x has a finite cycle trend described by some cycle factor and integer exponent m with (g^m)(a c) = x.

Русский

Для любого Basis a и x ∈ α либо x фиксирован g, либо существует цикл и целочисленный показатель m с (g^m)(a c) = x.

LaTeX

$$$x \in \mathrm{Fix}(g) \;\lor\; \exists c \in g.cycleFactorsFinset, \exists m \in \mathbb{Z}, (g^m)(a c) = x$$$

Lean4

/-- The function that will provide a right inverse `toCentralizer` to `toPermHom` -/
def ofPermHomFun (x : α) : α :=
  if hx : g.cycleOf x ∈ g.cycleFactorsFinset then
    (g ^ (Nat.find (a.sameCycle hx).exists_nat_pow_eq)) (a ((τ : Perm g.cycleFactorsFinset) ⟨g.cycleOf x, hx⟩))
  else x

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