l : Type ?u.381588
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
A✝ B : Matrix n n α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
this : Invertible (submatrix A ↑e₁ ↑e₂) := submatrixEquivInvertible A e₁ e₂
⊢ ⅟(submatrix A ↑e₁ ↑e₂) = submatrix ⅟A ↑e₂ ↑e₁
l : Type ?u.381588
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
A✝ B : Matrix n n α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
⊢ ⅟(submatrix A ↑e₁ ↑e₂) = submatrix ⅟A ↑e₂ ↑e₁
letI := submatrixEquivInvertible A e₁ e₂
no goals
l : Type ?u.381588
m : Type u
n : Type u'
α : Type v
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing α
A✝ B : Matrix n n α
inst✝³ : Fintype m
inst✝² : DecidableEq m
A : Matrix m m α
e₁ e₂ : n ≃ m
inst✝¹ : Invertible A
inst✝ : Invertible (submatrix A ↑e₁ ↑e₂)
this : Invertible (submatrix A ↑e₁ ↑e₂) := submatrixEquivInvertible A e₁ e₂
⊢ ⅟(submatrix A ↑e₁ ↑e₂) = submatrix ⅟A ↑e₂ ↑e₁
convert(rfl : ⅟ (A.submatrix e₁ e₂) = _)