English
For any finite list l, the alternating product of its reverse is equal to the alternating product of l raised to the power (-1)^{|l|+1}. Equivalently, alternatingProd(reverse l) = alternatingProd(l)^{(-1 : ℤ)^{|l|+1}}.
Русский
Для любого конечного списка l чередующее произведение обратного списка равно чередующему произведению самого списка, возведенному в степень (-1)^{|l|+1}.
LaTeX
$$$$ \operatorname{alternatingProd}(\operatorname{reverse}(l)) = \operatorname{alternatingProd}(l)^{(-1)^{|l|+1}}. $$$$
Lean4
@[to_additive]
theorem alternatingProd_reverse :
∀ l : List G, alternatingProd (reverse l) = alternatingProd l ^ (-1 : ℤ) ^ (length l + 1)
| [] => by simp only [alternatingProd_nil, one_zpow, reverse_nil]
| a :: l =>
by
simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse, alternatingProd_singleton,
alternatingProd_cons, length_reverse, length, pow_succ', Int.neg_mul, one_mul, zpow_neg, inv_inv]
rw [mul_comm, ← div_eq_mul_inv, div_zpow]
