R : Type u_3
inst✝¹ : CommSemiring R
k : Type ?u.315479
l : Type ?u.315482
m : Type u_1
n : Type u_2
inst✝ : Fintype n
M : Matrix m n R
this : DecidableEq n := Classical.decEq n
⊢ LinearMap.range (mulVecLin M) = span R (Set.range Mᵀ)
R : Type u_3
inst✝¹ : CommSemiring R
k : Type ?u.315479
l : Type ?u.315482
m : Type u_1
n : Type u_2
inst✝ : Fintype n
M : Matrix m n R
⊢ LinearMap.range (mulVecLin M) = span R (Set.range Mᵀ)
letI := Classical.decEq n
no goals
R : Type u_3
inst✝¹ : CommSemiring R
k : Type ?u.315479
l : Type ?u.315482
m : Type u_1
n : Type u_2
inst✝ : Fintype n
M : Matrix m n R
this : DecidableEq n := Classical.decEq n
⊢ LinearMap.range (mulVecLin M) = span R (Set.range Mᵀ)
simp_rw [range_eq_map, ← iSup_range_stdBasis, Submodule.map_iSup, range_eq_map, ←
  Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
  Matrix.mulVecLin_apply, M.mulVec_stdBasis_apply, iSup_span, range_eq_iUnion]