Theorems · Definition · functional analysis

NormedSpace.normalize

{V : Type u_1} → [inst : NormedAddCommGroup V] → [NormedSpace ℝ V] → V → V

For a nonzero vector x, normalize x is the unit-length vector that points in the same direction as x. If x = 0, then normalize x = 0.

Defined in

Mathlib.Analysis.Normed.Module.Normalize

Cited by

31 results in Mathlib

Foundations

Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace