n : Type ?u.145025
p : Type ?u.145028
q : Type ?u.145031
l : Type u_1
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 ⬝ 1 + 0 ⬝ 0) (1 ⬝ 0 + 0 ⬝ ⅟(PD l R)) (0 ⬝ 1 + PD l R ⬝ 0) (0 ⬝ 0 + 1) = 1
n : Type ?u.145025
p : Type ?u.145028
q : Type ?u.145031
l : Type u_1
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ PB l R * fromBlocks 1 0 0 ⅟(PD l R) = 1
rw [PB, Matrix.mul_eq_mul, Matrix.fromBlocks_multiply, Matrix.mul_invOf_self]
no goals
n : Type ?u.145025
p : Type ?u.145028
q : Type ?u.145031
l : Type u_1
R : Type u₂
inst✝⁸ : DecidableEq n
inst✝⁷ : DecidableEq p
inst✝⁶ : DecidableEq q
inst✝⁵ : DecidableEq l
inst✝⁴ : CommRing R
inst✝³ : Fintype p
inst✝² : Fintype q
inst✝¹ : Fintype l
inst✝ : Invertible 2
⊢ fromBlocks (1 ⬝ 1 + 0 ⬝ 0) (1 ⬝ 0 + 0 ⬝ ⅟(PD l R)) (0 ⬝ 1 + PD l R ⬝ 0) (0 ⬝ 0 + 1) = 1
simp only [Matrix.mul_zero, Matrix.mul_one, Matrix.zero_mul, zero_add, add_zero,
  Matrix.fromBlocks_one]