alternatingProd_cons' — Mathlib

English

For a group G, the alternating product of a :: l equals a times the inverse of the alternating product of l.

Русский

Для группы G произведение чередования списка, начинающегося с a, равно a умноженному на обратное чередование оставшегося списка.

LaTeX

$$$\forall a\ l,\ \\text{alternatingProd}(a :: l) = a * (\text{alternatingProd } l)^{-1}$$$

Lean4

@[to_additive]
theorem alternatingProd_cons' : ∀ (a : G) (l : List G), alternatingProd (a :: l) = a * (alternatingProd l)⁻¹
  | a, [] => by rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
  | a, b :: l => by rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]

Похожие утверждения