blockTriangular_transvection — Mathlib

English

The transvection matrix transvection i j c is block triangular with respect to b provided b i ≤ b j.

Русский

Матрица транспекция transvection i j c блочно-треугольна по b при условии b i ≤ b j.

LaTeX

$$$\BlockTriangular\bigl(\mathrm{transvection}\; i\; j\; c\bigr)\; b$ при $b i ≤ b j$$$

Lean4

theorem blockTriangular_transvection {i j : m} (hij : b i ≤ b j) (c : R) : BlockTriangular (transvection i j c) b :=
  blockTriangular_one.add (blockTriangular_single hij c)

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