add_iff_left — Mathlib

English

In an AddGroup, BlockTriangular (M+N) b is equivalent to BlockTriangular M b when N is BlockTriangular b.

Русский

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

LaTeX

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

Lean4

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

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