listTransvecCol_getElem — Mathlib

English

The matrix of the SumInl-constructed transvection equals a block matrix with the original matrix in the top-left and identity in the bottom-right block.

Русский

Матрица трансвеκции, полученной через SumInl, образует блочную матрицу: исходная матрица в верхнем левом блоке и единичная — в нижнем правом.

LaTeX

$$$(t.sumInl p).toMatrix = \\mathrm{fromBlocks}(t.toMatrix, 0, 0, 1)$$$

Lean4

theorem listTransvecCol_getElem {i : ℕ} (h : i < (listTransvecCol M).length) :
    (listTransvecCol M)[i] =
      letI i' : Fin r := ⟨i, length_listTransvecCol M ▸ h⟩
      transvection (inl i') (inr unit) <| -M (inl i') (inr unit) / M (inr unit) (inr unit) :=
  by simp [listTransvecCol]

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