reverse_prod_map_ι — Mathlib

English

For a list l of vectors, reversing the product of their lifted images equals the product of the lifted images taken in reverse order.

Русский

Для списка векторов произведение их образов через ι Q, взятое с изменением порядка, при обратке сохраняется в обратном порядке.

LaTeX

$$$ reverse( (l.map (\ι Q)).prod ) = (l.map (\ι Q)).reverse.prod $$$

Lean4

/-- Taking the reverse of the product a list of $n$ vectors lifted via `ι` is equivalent to
taking the product of the reverse of that list. -/
theorem reverse_prod_map_ι : ∀ l : List M, reverse (l.map <| ι Q).prod = (l.map <| ι Q).reverse.prod
  | [] => by simp
  | x :: xs => by simp [reverse_prod_map_ι xs]

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