involute_prod_map_ι — Mathlib

English

For any list l, the involute of the lifted product equals (-1) raised to the length of the list times the lifted product.

Русский

Для любого списка l инфлуента (обратная) произведения образов через ι Q равно (-1)^{|l|} умноженному на то же произведение.

LaTeX

$$$ involute( (l.map (\ι Q)).prod ) = (-1)^{|l|} \; (l.map (\ι Q)).prod $$$

Lean4

/-- Taking the involute of the product a list of $n$ vectors lifted via `ι` is equivalent to
premultiplying by ${-1}^n$. -/
theorem involute_prod_map_ι : ∀ l : List M, involute (l.map <| ι Q).prod = (-1 : R) ^ l.length • (l.map <| ι Q).prod
  | [] => by simp
  | x :: xs => by simp [pow_succ, involute_prod_map_ι xs]

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