Normalizing a vector

Stream: Is there code for X?

[Yaël Dillies]

Do we have this anywhere?

import analysis.normed_space.basic

variables {E : Type*} [normed_group E] [normed_space ℝ E]

noncomputable def normalize_vector (x : E) : E := ∥x∥⁻¹ • x

[Oliver Nash]

I don't see it. I note it is inlined in docs#gram_schmidt_normed

[Yaël Dillies]

Yes, exactly. The context is #14514

[Yaël Dillies]

I'm particularly interested in the fact that span 𝕜 {normalize_vector x} = span 𝕜 {x}.

[Yaël Dillies]

and more generally span 𝕜 (normalize_vector '' s) = span 𝕜 s.

[Yaël Dillies]

Does this deserve its own definition? I want to say yes, because it already is used in more specific contexts.

[Oliver Nash]

I'd lean in favour.

[Eric Wieser]

Is there more general statement that span 𝕜 {k • x} = span 𝕜 {x} when k is not 0?

[Kevin Buzzard]

This is not more general because ∥x∥⁻¹ = 0 when x = 0. Says the pedant.

[Yaël Dillies]

Yes, I precisely want to avoid casing on whether x is zero or not.