Scalar product in Euclidean space

Stream: new members

[Michael Novak]

I'm working with vectors in EuclideanSpace ℝ (Fin 2) and I want to use a theorem like theorem Matrix.smul_vec2 but for the Euclidean space I'm working with. How can I do this?

[Aaron Liu]

docs#Matrix.smul_vec2

[Aaron Liu]

can you give a #mwe?

[Eric Wieser]

Perhaps

import Mathlib

example (c x y : ℝ) : c • !₂[x, y] = sorry := by
  rw [← WithLp.toLp_smul, Matrix.smul_vec2]

[Michael Novak]

Eric Wieser said:

Perhaps

import Mathlib

example (c x y : ℝ) : c • !₂[x, y] = sorry := by
  rw [← WithLp.toLp_smul, Matrix.smul_vec2]

That's exactly what I was looking for, thank you very much!

[Michael Novak]

Aaron Liu said:

docs#Matrix.smul_vec2

Sorry, I was away from my computer for a few hours, but as you can see my question was answered. Thank you very much for trying to help!