list_prod_inv_reverse — Mathlib

English

For any list of matrices, the inverse of the product equals the product of the inverses in reverse order.

Русский

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

LaTeX

$$l.prod^{-1} = (l.reverse.map Inv.inv).prod$$

Lean4

/-- A version of `List.prod_inv_reverse` for `Matrix.inv`. -/
theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.reverse.map Inv.inv).prod
  | [] => by rw [List.reverse_nil, List.map_nil, List.prod_nil, inv_one]
  | A :: Xs => by
    rw [List.reverse_cons', List.map_concat, List.prod_concat, List.prod_cons, mul_inv_rev, list_prod_inv_reverse Xs]

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