English
In a group G, for f: Fin(n+1) → G, the element f(0) multiplied by the partialProd of ((f i.castSucc)^{-1} · f i.succ) over i ∈ Fin n yields f.
Русский
Для группы G и функции f: Fin(n+1) → G произведение f(0) умноженное на частичное произведение последовательности ((f i.castSucc)^{-1} · f i.succ) даёт f.
LaTeX
$$$$f(0) \\cdot \\Big( \\prod_{i \\in Fin\,n} \\big( (f(i.castSucc))^{-1} \\cdot f(i.succ) \\big) \\Big) = f.$$$$
Lean4
@[to_additive]
theorem partialProd_left_inv {G : Type*} [Group G] (f : Fin (n + 1) → G) :
(f 0 • partialProd fun i : Fin n => (f i.castSucc)⁻¹ * f i.succ) = f :=
funext fun x =>
Fin.inductionOn x (by simp) fun x hx =>
by
simp only [Pi.smul_apply, smul_eq_mul] at hx ⊢
rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]
