toMatrix_mk — Mathlib

English

The matrix corresponding to the constructed TransvectionStruct ⟨i, j, hij, c⟩ is exactly the transvection with indices i, j and value c.

Русский

Матрица, соответствующая структуры TransvectionStruct ⟨i, j, hij, c⟩, равна трансвеκции с индексами i, j и значением c.

LaTeX

$$$\\text{toMatrix}(\\langle i,j,hij,c\\rangle) = \\operatorname{transvection}(i,j,c)$$$

Lean4

@[simp]
theorem toMatrix_mk (i j : n) (hij : i ≠ j) (c : R) : TransvectionStruct.toMatrix ⟨i, j, hij, c⟩ = transvection i j c :=
  rfl

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