English
Let g be a group element whose powers generate a cyclic subgroup ⟨g⟩. If x ∈ G →₀ k satisfies leftRegular g x = x, then for every γ in ⟨g⟩ one has x(γ) = x(g).
Русский
Пусть g порождает циклическую подгруппу ⟨g⟩. Если x ∈ G →₀ k удовлетворяет leftRegular g x = x, то для любого γ ∈ ⟨g⟩ выполняется x(γ) = x(g).
LaTeX
$$$ \\forall \\gamma \\in \\langle g \\rangle:\\; x(\\gamma) = x(g) $$$
Lean4
theorem apply_eq_of_leftRegular_eq_of_generator (g : G) (hg : ∀ x, x ∈ Subgroup.zpowers g) (x : G →₀ k)
(hx : leftRegular k G g x = x) (γ : G) : x γ = x g :=
by
rcases hg γ with ⟨i, rfl⟩
induction i with
| zero => simpa using (Finsupp.ext_iff.1 hx g)
| succ n h =>
simpa [← h, zpow_natCast, zpow_add_one, pow_mul_comm', pow_succ'] using (Finsupp.ext_iff.1 hx (g ^ (n + 1))).symm
| pred n h => simpa [zpow_sub, ← h, ← mul_inv_rev, ← pow_mul_comm'] using Finsupp.ext_iff.1 hx (g ^ (-n : ℤ))
