no goals
R : Type ?u.2867092
R₁ : Type u_2
R₂ : Type ?u.2867098
M✝ : Type ?u.2867101
M₁ : Type ?u.2867104
M₂ : Type ?u.2867107
M₁' : Type ?u.2867110
M₂' : Type ?u.2867113
n : Type ?u.2867116
m : Type ?u.2867119
n' : Type ?u.2867122
m' : Type ?u.2867125
ι : Type u_1
inst✝⁵ : CommRing R₁
inst✝⁴ : AddCommMonoid M₁
inst✝³ : Module R₁ M₁
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁
inst✝ : IsDomain R₁
M : Matrix ι ι R₁
⊢ SeparatingLeft (↑toLinearMap₂' M) ↔ det M ≠ 0
rw [Matrix.separatingLeft_toLinearMap₂'_iff, Matrix.nondegenerate_iff_det_ne_zero]