English
For a cycle σ, the z-powers equivalence applied to ⟨σ^n, n, rfl⟩ yields the pair consisting of (σ^n) evaluated at a chosen representative and a membership certificate in the support.
Русский
Для цикла σ отображение z-поков-множительствует к паре ⟨σ^n, n, rfl⟩ равен паре, где первый элемент — это σ^n, применённый к выбранному представителю, и второй — член принадлежности к опоре.
LaTeX
$$$ h\\sigma . zpowersEquivSupport \\langle σ^n, n, rfl \\rangle = \\langle (σ^n)(\\text{Classical.choose } hσ), \\text{pow\_apply\_mem\_support.2 (mem\_support.2 (Classical.choose\_spec hσ).1)} \\rangle $$$
Lean4
@[simp]
theorem zpowersEquivSupport_apply {σ : Perm α} (hσ : IsCycle σ) {n : ℕ} :
hσ.zpowersEquivSupport ⟨σ ^ n, n, rfl⟩ =
⟨(σ ^ n) (Classical.choose hσ), pow_apply_mem_support.2 (mem_support.2 (Classical.choose_spec hσ).1)⟩ :=
rfl
