transvection — Mathlib

English

The transvection matrix T_{ij}(c) is equal to the identity plus c in position (i,j).

Русский

Транспективная матрица T_{ij}(c) равна единичной матрице плюс c в позиции (i,j).

LaTeX

$$$$ \\mathrm{transvection}_{ij}(c) = I + c \\, E_{ij}, $$$$

Lean4

/-- The transvection matrix `transvection i j c` is equal to the identity plus `c` at position
`(i, j)`. Multiplying by it on the left (as in `transvection i j c * M`) corresponds to adding
`c` times the `j`-th row of `M` to its `i`-th row. Multiplying by it on the right corresponds
to adding `c` times the `i`-th column to the `j`-th column. -/
def transvection (c : R) : Matrix n n R :=
  1 + Matrix.single i j c

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