Theorem: MatrixCookbook.eq_401 (MatrixCookbook/9SpecialMatrices.lean)

State before:
R : Type u_2
l : Type ?u.78563
m : Type u_1
n : Type u_3
p : Type ?u.78572
q : Type ?u.78575
r : Type ?u.78578
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A₁₁ : Matrix m m R
A₂₂ : Matrix n n R
h : IsUnit A₁₁ ↔ IsUnit A₂₂
⊢ A₁₁⁻¹.fromBlocks 0 (-(A₂₂⁻¹ * 0 * A₁₁⁻¹)) A₂₂⁻¹ = A₁₁⁻¹.fromBlocks 0 0 A₂₂⁻¹
Tactic:
simp
State after:
no goals