alternatingProd_cons — Mathlib

English

For a group G, the alternating product of a :: l equals a / alternatingProd l.

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem alternatingProd_cons (a : G) (l : List G) : alternatingProd (a :: l) = a / alternatingProd l := by
  rw [div_eq_mul_inv, alternatingProd_cons']

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