neg — Mathlib

English

If M is BlockTriangular with respect to b and R has a NegZero structure, then -M is BlockTriangular with respect to the same b.

Русский

Если M блочно-треугольна относительно b и у R имеется свойство NegZero, то -M также блочно-треугольна относительно той же разметки.

LaTeX

$$$\BlockTriangular\, M\; b \Rightarrow \BlockTriangular\;(-M)\; b$$$

Lean4

protected theorem neg [NegZeroClass R] {M : Matrix m m R} (hM : BlockTriangular M b) : BlockTriangular (-M) b :=
  fun _ _ h => by rw [neg_apply, hM h, neg_zero]

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