prod_reverse_noncomm — Mathlib

English

In a group, the product taken in reverse order equals the inverse of the product of the original inverses in the original order.

Русский

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

LaTeX

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

Lean4

/-- A non-commutative variant of `List.prod_reverse` -/
@[to_additive /-- A non-commutative variant of `List.sum_reverse` -/
    ]
theorem prod_reverse_noncomm : ∀ L : List G, L.reverse.prod = (L.map fun x => x⁻¹).prod⁻¹ := by simp [prod_inv_reverse]

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