Documentation

Mathlib.Analysis.NormedSpace.Normalize

Normalized vector #

Function that returns unit length vector that points in the same direction (if the given vector is nonzero vector) or returns zero vector (if the given vector is zero vector).

source
noncomputable def NormedSpace.normalize {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : 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.

Equations
Instances For
    source
    @[simp]
    theorem NormedSpace.normalize_zero_eq_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] :
    normalize 0 = 0
    source
    @[simp]
    theorem NormedSpace.norm_smul_normalize {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V) :
    ‖x‖ • normalize x = x
    source
    @[simp]
    theorem NormedSpace.norm_normalize_eq_one_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {x : V} :
    ‖normalize x‖ = 1 ↔ x ≠ 0
    source
    theorem NormedSpace.normalize_eq_self_of_norm_eq_one {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {x : V} (h : ‖x‖ = 1) :
    normalize x = x
    source
    @[simp]
    theorem NormedSpace.normalize_normalize {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V) :
    normalize (normalize x) = normalize x
    source
    @[simp]
    theorem NormedSpace.normalize_neg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (x : V) :
    normalize (-x) = -normalize x
    source
    theorem NormedSpace.normalize_smul_of_pos {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {r : ℝ} (hr : 0 < r) (x : V) :
    normalize (r • x) = normalize x
    source
    theorem NormedSpace.normalize_smul_of_neg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {r : ℝ} (hr : r < 0) (x : V) :
    normalize (r • x) = -normalize x