prod_inv_reverse — Mathlib

English

For any finite list L in a group, the inverse of the product of its elements equals the product of their inverses taken in the reverse order.

Русский

Для любого конечного списка L в группе, обратное произведение элементов списка равно произведению обратных элементов, взятых в обратном порядке.

LaTeX

$$$L.prod^{-1} = (L.map (\x ↦ x^{-1})).reverse.prod$$

Lean4

/-- This is the `List.prod` version of `mul_inv_rev` -/
@[to_additive /-- This is the `List.sum` version of `add_neg_rev` -/
    ]
theorem prod_inv_reverse : ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).reverse.prod
  | [] => by simp
  | x :: xs => by simp [prod_inv_reverse xs]

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