English
For a noncommutative setting over a DivisionMonoid, the alternating product of a list equals the finite product over indices i of L[i] raised to (−1)^i.
Русский
В разделе с делением (DivisionMonoid) чередующееся произведение списка равно конечному произведению по индексам i из L[i], возведённых в (−1)^i.
LaTeX
$$$L\\text{.alternatingProd} = \\prod_{i:\\mathrm{Fin}\\ L.length} L[i]^{(-1)^i}$$$
Lean4
@[to_additive]
theorem alternatingProd_eq_finset_prod {G : Type*} [DivisionCommMonoid G] :
∀ (L : List G), alternatingProd L = ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ)
| [] => by
rw [alternatingProd, Finset.prod_eq_one]
rintro ⟨i, ⟨⟩⟩
| g :: [] => by
change g = ∏ i : Fin 1, [g][i] ^ (-1 : ℤ) ^ (i : ℕ)
rw [Fin.prod_univ_succ]; simp
| g :: h :: L =>
calc
g * h⁻¹ * L.alternatingProd = g * h⁻¹ * ∏ i : Fin L.length, L[i] ^ (-1 : ℤ) ^ (i : ℕ) :=
congr_arg _ (alternatingProd_eq_finset_prod _)
_ = ∏ i : Fin (L.length + 2), (g :: h :: L)[i] ^ (-1 : ℤ) ^ (i : ℕ) := by
{
rw [Fin.prod_univ_succ, Fin.prod_univ_succ, mul_assoc]
simp [pow_add]
}
