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.

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

Coercion ℝ → angle as an additive homomorphism.

Equations
@[protected]
theorem real.angle.induction_on {p : real.angle → Prop} (θ : real.angle) (h : ∀ (x : ), p x) :
p θ

An induction principle to deduce results for angle from those for , used with induction θ using real.angle.induction_on.

@[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.coe_two_pi  :
(2 * real.pi) = 0
theorem real.angle.cos_sin_inj {θ ψ : } (Hcos : real.cos θ = real.cos ψ) (Hsin : real.sin θ = real.sin ψ) :
θ = ψ
noncomputable def real.angle.sin (θ : real.angle) :

The sine of a real.angle.

Equations
@[simp]
theorem real.angle.sin_coe (x : ) :
noncomputable def real.angle.cos (θ : real.angle) :

The cosine of a real.angle.

Equations
@[simp]
theorem real.angle.cos_coe (x : ) :