prod_pow_eq_one — Mathlib

English

Let φ be fixed-point-free and φ^n = id. Then for every g ∈ G, the product ∏_{k=0}^{n-1} φ^k(g) equals the identity.

Русский

Пусть φ — фикс-фри и φ^n = id. Тогда для каждого g ∈ G произведение ∏_{k=0}^{n-1} φ^k(g) равно единице.

LaTeX

$$$\text{FixedPointFree}(\varphi) \land φ^{n}=\mathrm{id} \Rightarrow \prod_{k=0}^{n-1} φ^{k}(g) = e$$$

Lean4

theorem prod_pow_eq_one (hφ : FixedPointFree φ) {n : ℕ} (hn : φ^[n] = _root_.id) (g : G) :
    ((List.range n).map (fun k ↦ φ^[k] g)).prod = 1 :=
  by
  obtain ⟨g, rfl⟩ := commutatorMap_surjective hφ g
  simp only [commutatorMap_apply, iterate_map_div, ← Function.iterate_succ_apply]
  rw [List.prod_range_div', Function.iterate_zero_apply, hn, Function.id_def, div_self']

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