listTransvecCol — Mathlib

English

A variant of the product identities: the product of L.map toMatrix times the reverse of the product of their inverses equals 1.

Русский

Вариант тождества произведений: произведение L.map toMatrix умноженное на обратное произведение их инверсий равно единице.

LaTeX

$$(L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ inv)).prod = 1$$

Lean4

/-- A list of transvections such that multiplying on the left with these transvections will replace
the last column with zeroes. -/
def listTransvecCol : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i : Fin r => transvection (inl i) (inr unit) <| -M (inl i) (inr unit) / M (inr unit) (inr unit)

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