add_iff_right — Mathlib

English

In an AddGroup, if M is BlockTriangular with respect to b, then M+N is BlockTriangular with respect to b iff N is BlockTriangular with respect to b.

Русский

В группе сложения, если M блочно-треугольна по b, то (M+N) блочно-треугольна по b тогда и только тогда, когда N блочно-треугольна по b.

LaTeX

$$$\text{BlockTriangular}(M,b) \Rightarrow (\BlockTriangular(M+N,b) \iff \BlockTriangular(N,b)))$$$

Lean4

theorem add_iff_right [AddGroup R] (hM : BlockTriangular M b) : BlockTriangular (M + N) b ↔ BlockTriangular N b :=
  ⟨(by simpa using hM.neg.add ·), hM.add⟩

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