listTransvecRow_getElem — Mathlib

English

The list of row transvections has length r.

Русский

Список строковых трансвеκций имеет длину r.

LaTeX

$$$(\\text{listTransvecRow }M).\\text{length} = r$$$

Lean4

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

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