∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] (m : 𝕜)
  (x : EuclideanSpace 𝕜 n →ₗ[𝕜] EuclideanSpace 𝕜 n),
  (↑LinearMap.toContinuousLinearMap).toFun (m • x) = (RingHom.id 𝕜) m • (↑LinearMap.toContinuousLinearMap).toFun x