blockTriangular_transvection' — Mathlib

English

If b j ≤ b i, then transvection i j c is block triangular with respect to OrderDual ∘ b.

Русский

Если b j ≤ b i, то транспекция i j c блочно-треугольна относительно OrderDual ∘ b.

LaTeX

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

Lean4

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

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