alternatingProd_cons_cons — Mathlib

English

For a group G, the alternating product of a :: b :: l equals (a / b) times the alternating product of l.

Русский

Для группы G чередующее произведение {a, b, l} равно (a / b) умножить на чередующее произведение l.

LaTeX

$$$\text{alternatingProd} (a :: b :: l) = a / b * \text{alternatingProd} l$$$

Lean4

@[to_additive]
theorem alternatingProd_cons_cons [DivInvMonoid G] (a b : G) (l : List G) :
    alternatingProd (a :: b :: l) = a / b * alternatingProd l := by rw [div_eq_mul_inv, alternatingProd_cons_cons']

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