no goals
R : Type ?u.2676271
R₁ : Type u_2
R₂ : Type ?u.2676277
M✝ : Type ?u.2676280
M₁ : Type ?u.2676283
M₂ : Type ?u.2676286
M₁' : Type ?u.2676289
M₂' : Type ?u.2676292
n : Type ?u.2676295
m : Type ?u.2676298
n' : Type ?u.2676301
m' : Type ?u.2676304
ι : Type u_1
inst✝⁴ : CommRing R₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
B : M₁ →ₗ[R₁] M₁ →ₗ[R₁] R₁
M : Matrix ι ι R₁
h : Matrix.Nondegenerate M
x : ι → R₁
hx : ∀ (y : ι → R₁), ↑(↑(↑Matrix.toLinearMap₂' M) x) y = 0
y : ι → R₁
⊢ x ⬝ᵥ mulVec M y = 0
simpa only [toLinearMap₂'_apply'] using hx y