English
The list of column-transvections is constructed by indexing over Fin r, producing a transvection for each i with i ≠ j and a scalar derived from M.
Русский
Список столбцовых трансвеκций строится по индексации через Fin r, порождая трансвеκцию для каждого i при i ≠ j и скаляром, получаемым из M.
LaTeX
$$$\\text{listTransvecCol }M = \\text{List.ofFn }(i:\\mathrm{Fin}\;r \\mapsto \\operatorname{transvection}(\\mathrm{inl}(i),\\mathrm{inr}(\\mathrm{unit}))\\big(-M(\\mathrm{inl}(i),\\mathrm{inr}(\\mathrm{unit}))/M(\\mathrm{inr}(\\mathrm{unit}),\\mathrm{inr}(\\mathrm{unit}))\\big))$$$
Lean4
/-- A list of transvections such that multiplying on the right with these transvections will replace
the last row with zeroes. -/
def listTransvecRow : List (Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) :=
List.ofFn fun i : Fin r => transvection (inr unit) (inl i) <| -M (inr unit) (inl i) / M (inr unit) (inr unit)
