letI := hA.invertible
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A
m : Type ?u.28189
n : Type u_1
p : Type ?u.28195
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : Fintype p
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq p
A B C : Matrix n n ℂ
hA : IsUnit A
hB : IsUnit B
this : Invertible A := hA.invertible
⊢ (A⁻¹ + B⁻¹)⁻¹ = A * (A + B)⁻¹ * B ∧ (A⁻¹ + B⁻¹)⁻¹ = B * (A + B)⁻¹ * A