English
For a representation ρ of a finite group G, and for the partial sums of the orbit ρ(g^j)x, applying ρ(g) minus the identity to the last partial sum equals ρ(g^{n+1})x − x.
Русский
Для конечной группы G и частичных сумм орбиты ρ(g^j)x операция ρ(g)−id на последнюю частичную сумму даёт ρ(g^{n+1})x−x.
LaTeX
$$$\\big(\\rho(g) - \\mathrm{Id}_V\\big)\\Big(\\mathrm{Fin.last} \\; \\% (n+1) \\cdot ρ(g^j) x\\Big) = ρ(g^{n+1}) x - x$$$
Lean4
theorem apply_sub_id_partialSum_eq (n : ℕ) (g : G) (x : V) :
(ρ g - LinearMap.id (R := k) (M := V)) ((Fin.last _).partialSum (fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) x)) =
ρ (g ^ (n + 1)) x - x :=
by
induction n with
| zero => simp [Fin.partialSum]
| succ n
h =>
have : Fin.init (fun (j : Fin (n + 2)) => ρ (g ^ (j : ℕ)) x) = fun (j : Fin (n + 1)) => ρ (g ^ (j : ℕ)) x := by ext;
simp [Fin.init]
rw [← Fin.succ_eq_last_succ.2 rfl, Fin.partialSum_succ, ← Fin.partialSum_init, map_add, this, h]
simp [pow_succ']
