mathlib documentation

analysis.special_functions.trigonometric.angle

The type of angles #

In this file we define real.angle to be the quotient group ℝ/2πℤ and prove a few simple lemmas about trigonometric functions and angles.

def real.angle  :
Type

The type of angles

Equations
@[protected, instance]
noncomputable def real.angle.inhabited  :
Equations
noncomputable def real.angle.coe_hom  :

Coercion ℝ → angle as an additive homomorphism.

Equations
@[simp]
theorem real.angle.coe_zero  :
0 = 0
@[simp]
theorem real.angle.coe_add (x y : ) :
(x + y) = x + y
@[simp]
theorem real.angle.coe_neg (x : ) :
@[simp]
theorem real.angle.coe_sub (x y : ) :
(x - y) = x - y
@[simp, norm_cast]
theorem real.angle.coe_nat_mul_eq_nsmul (x : ) (n : ) :
(n) * x = n x
@[simp, norm_cast]
theorem real.angle.coe_int_mul_eq_zsmul (x : ) (n : ) :
(n) * x = n x
theorem real.angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : } :
θ = ψ ∃ (k : ), θ - ψ = (2 * real.pi) * k
@[simp]
theorem real.angle.cos_sin_inj {θ ψ : } (Hcos : real.cos θ = real.cos ψ) (Hsin : real.sin θ = real.sin ψ) :
θ = ψ