English
Let G be a group and g: Fin(n+1) → G. For j: Fin(n+1) and k: Fin n, the equation relates the left quotient of two partial products to the contracted element j.contractNth(·*·) g k.
Русский
Пусть G — группа, g: Fin(n+1) → G. Для j: Fin(n+1) и k: Fin n существует равенство, связывающее левый частный частичного произведения через контрактированный элемент.
LaTeX
$$$$\\left(\\partialProd\ng( j.succ.succAbove k.castSucc)\\right)^{-1} \\cdot \\partialProd g (j.succAbove k).succ = j.contractNth(\\cdot * \\cdot) g k.$$$$
Lean4
@[to_additive]
theorem partialProd_right_inv {G : Type*} [Group G] (f : Fin n → G) (i : Fin n) :
(partialProd f (Fin.castSucc i))⁻¹ * partialProd f i.succ = f i := by rw [partialProd_succ, inv_mul_cancel_left]
