no goals
R : Type ?u.2919829
R₁ : Type u_1
R₂ : Type ?u.2919835
M : Type ?u.2919838
M₁ : Type u_2
M₂ : Type ?u.2919844
M₁' : Type ?u.2919847
M₂' : Type ?u.2919850
n : Type ?u.2919853
m : Type ?u.2919856
n' : Type ?u.2919859
m' : Type ?u.2919862
ι : Type u_3
inst✝⁵ : CommRing R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
B✝ : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁
inst✝ : IsDomain R₁
B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁
b : Basis ι R₁ M₁
⊢ SeparatingLeft B ↔ det (↑(toMatrix₂ b b) B) ≠ 0
rw [← Matrix.nondegenerate_iff_det_ne_zero, nondegenerate_toMatrix_iff]