pb_inv — Mathlib

English

PB(l,R) is invertible in the corresponding matrix algebra, with inverse realized via a right-inverse construction from PD.

Русский

PB(l,R) инвертируемая в соответствующей алгебре матриц, обратная реализуется через правую обратность для PD.

LaTeX

$$$ PB(l,R) \text{ invertible}.$$$

Lean4

theorem pb_inv [Invertible (2 : R)] : PB l R * Matrix.fromBlocks 1 0 0 (⅟(PD l R)) = 1 :=
  by
  rw [PB, Matrix.fromBlocks_multiply, mul_invOf_self]
  simp only [Matrix.mul_zero, Matrix.mul_one, Matrix.zero_mul, zero_add, add_zero, Matrix.fromBlocks_one]

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