IsClosedMap mulVec

Stream: Is there code for X?

[Apurva Nakade]

I have one final thing remaining to show about matrices for one of my proofs:

import Mathlib.Data.Matrix.Basic
import Mathlib.Topology.UniformSpace.Pi
import Mathlib.Analysis.InnerProductSpace.PiL2

open Matrix

example {n m : Type*} [Fintype n] [Fintype m] (A : Matrix m n ℝ) :
  IsClosedMap (mulVec A) := sorry

Is there some slick way to do this using existing results in the library?

[Apurva Nakade]

(deleted)