toMatrix — Mathlib

English

For any TransvectionStruct t, the associated matrix t.toMatrix is exactly the corresponding transvection matrix given by i, j and c.

Русский

Для любого TransvectionStruct t ассоциированная матрица t.toMatrix равна соответствующей матрице трансвеκции, заданной i, j и c.

LaTeX

$$$\\forall t:\\text{TransvectionStruct }n\\,R,\\; t.toMatrix = \\operatorname{transvection}(t.i,t.j,t.c)$$$

Lean4

/-- Associating to a `transvection_struct` the corresponding transvection matrix. -/
def toMatrix (t : TransvectionStruct n R) : Matrix n n R :=
  transvection t.i t.j t.c

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