# mathlib3documentation

geometry.euclidean.angle.unoriented.basic

# Angles between vectors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines unoriented angles in real inner product spaces.

## Main definitions #

• inner_product_geometry.angle is the undirected angle between two vectors.
noncomputable def inner_product_geometry.angle {V : Type u_1} (x y : V) :

The undirected angle between two vectors. If either vector is 0, this is π/2. See orientation.oangle for the corresponding oriented angle definition.

Equations
theorem inner_product_geometry.continuous_at_angle {V : Type u_1} {x : V × V} (hx1 : x.fst 0) (hx2 : x.snd 0) :
continuous_at (λ (y : V × V), x
theorem inner_product_geometry.angle_smul_smul {V : Type u_1} {c : } (hc : c 0) (x y : V) :
(c y) =
@[simp]
theorem linear_isometry.angle_map {E : Type u_1} {F : Type u_2} (f : E →ₗᵢ[] F) (u v : E) :
(f v) =
@[simp, norm_cast]
theorem submodule.angle_coe {V : Type u_1} {s : V} (x y : s) :
theorem inner_product_geometry.cos_angle {V : Type u_1} (x y : V) :

The cosine of the angle between two vectors.

theorem inner_product_geometry.angle_comm {V : Type u_1} (x y : V) :

The angle between two vectors does not depend on their order.

@[simp]
theorem inner_product_geometry.angle_neg_neg {V : Type u_1} (x y : V) :

The angle between the negation of two vectors.

theorem inner_product_geometry.angle_nonneg {V : Type u_1} (x y : V) :

The angle between two vectors is nonnegative.

theorem inner_product_geometry.angle_le_pi {V : Type u_1} (x y : V) :

The angle between two vectors is at most π.

theorem inner_product_geometry.angle_neg_right {V : Type u_1} (x y : V) :

The angle between a vector and the negation of another vector.

theorem inner_product_geometry.angle_neg_left {V : Type u_1} (x y : V) :

The angle between the negation of a vector and another vector.

@[simp]
theorem inner_product_geometry.angle_zero_left {V : Type u_1} (x : V) :

The angle between the zero vector and a vector.

@[simp]
theorem inner_product_geometry.angle_zero_right {V : Type u_1} (x : V) :

The angle between a vector and the zero vector.

@[simp]
theorem inner_product_geometry.angle_self {V : Type u_1} {x : V} (hx : x 0) :

The angle between a nonzero vector and itself.

@[simp]
theorem inner_product_geometry.angle_self_neg_of_nonzero {V : Type u_1} {x : V} (hx : x 0) :

The angle between a nonzero vector and its negation.

@[simp]
theorem inner_product_geometry.angle_neg_self_of_nonzero {V : Type u_1} {x : V} (hx : x 0) :

The angle between the negation of a nonzero vector and that vector.

@[simp]
theorem inner_product_geometry.angle_smul_right_of_pos {V : Type u_1} (x y : V) {r : } (hr : 0 < r) :

The angle between a vector and a positive multiple of a vector.

@[simp]
theorem inner_product_geometry.angle_smul_left_of_pos {V : Type u_1} (x y : V) {r : } (hr : 0 < r) :

The angle between a positive multiple of a vector and a vector.

@[simp]
theorem inner_product_geometry.angle_smul_right_of_neg {V : Type u_1} (x y : V) {r : } (hr : r < 0) :
(r y) =

The angle between a vector and a negative multiple of a vector.

@[simp]
theorem inner_product_geometry.angle_smul_left_of_neg {V : Type u_1} (x y : V) {r : } (hr : r < 0) :
y =

The angle between a negative multiple of a vector and a vector.

The cosine of the angle between two vectors, multiplied by the product of their norms.

theorem inner_product_geometry.sin_angle_mul_norm_mul_norm {V : Type u_1} (x y : V) :
* (x * y) = x * - * y)

The sine of the angle between two vectors, multiplied by the product of their norms.

theorem inner_product_geometry.angle_eq_zero_iff {V : Type u_1} {x y : V} :
x 0 (r : ), 0 < r y = r x

The angle between two vectors is zero if and only if they are nonzero and one is a positive multiple of the other.

theorem inner_product_geometry.angle_eq_pi_iff {V : Type u_1} {x y : V} :
x 0 (r : ), r < 0 y = r x

The angle between two vectors is π if and only if they are nonzero and one is a negative multiple of the other.

theorem inner_product_geometry.angle_add_angle_eq_pi_of_angle_eq_pi {V : Type u_1} {x y : V} (z : V) (h : = real.pi) :

If the angle between two vectors is π, the angles between those vectors and a third vector add to π.

Two vectors have inner product 0 if and only if the angle between them is π/2.

If the angle between two vectors is π, the inner product equals the negative product of the norms.

If the angle between two vectors is 0, the inner product equals the product of the norms.

theorem inner_product_geometry.inner_eq_neg_mul_norm_iff_angle_eq_pi {V : Type u_1} {x y : V} (hx : x 0) (hy : y 0) :

The inner product of two non-zero vectors equals the negative product of their norms if and only if the angle between the two vectors is π.

theorem inner_product_geometry.inner_eq_mul_norm_iff_angle_eq_zero {V : Type u_1} {x y : V} (hx : x 0) (hy : y 0) :

The inner product of two non-zero vectors equals the product of their norms if and only if the angle between the two vectors is 0.

If the angle between two vectors is π, the norm of their difference equals the sum of their norms.

If the angle between two vectors is 0, the norm of their sum equals the sum of their norms.

If the angle between two vectors is 0, the norm of their difference equals the absolute value of the difference of their norms.

theorem inner_product_geometry.norm_sub_eq_add_norm_iff_angle_eq_pi {V : Type u_1} {x y : V} (hx : x 0) (hy : y 0) :

The norm of the difference of two non-zero vectors equals the sum of their norms if and only the angle between the two vectors is π.

theorem inner_product_geometry.norm_add_eq_add_norm_iff_angle_eq_zero {V : Type u_1} {x y : V} (hx : x 0) (hy : y 0) :

The norm of the sum of two non-zero vectors equals the sum of their norms if and only the angle between the two vectors is 0.

theorem inner_product_geometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero {V : Type u_1} {x y : V} (hx : x 0) (hy : y 0) :

The norm of the difference of two non-zero vectors equals the absolute value of the difference of their norms if and only the angle between the two vectors is 0.

The norm of the sum of two vectors equals the norm of their difference if and only if the angle between them is π/2.

The cosine of the angle between two vectors is 1 if and only if the angle is 0.

The cosine of the angle between two vectors is 0 if and only if the angle is π / 2.

The cosine of the angle between two vectors is -1 if and only if the angle is π.

The sine of the angle between two vectors is 0 if and only if the angle is 0 or π.

The sine of the angle between two vectors is 1 if and only if the angle is π / 2.