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.

source
def real.angle  :
Type

The type of angles

Equations
source
@[protected, instance]
noncomputable def real.angle.angle.add_comm_group  :
add_comm_group real.angle
Equations
source
@[protected, instance]
noncomputable def real.angle.inhabited  :
inhabited real.angle
Equations
source
@[protected, instance]
noncomputable def real.angle.has_coe  :
has_coe ℝ real.angle
Equations
source
noncomputable def real.angle.coe_hom  :
ℝ →+ real.angle

Coercion ℝ → angle as an additive homomorphism.

Equations
source
@[simp]
theorem real.angle.coe_coe_hom  :
⇑real.angle.coe_hom = coe
source
@[simp]
theorem real.angle.coe_zero  :
↑0 = 0
source
@[simp]
theorem real.angle.coe_add (x y : ℝ) :
↑(x + y) = ↑x + ↑y
source
@[simp]
theorem real.angle.coe_neg (x : ℝ) :
↑-x = -↑x
source
@[simp]
theorem real.angle.coe_sub (x y : ℝ) :
↑(x - y) = ↑x - ↑y
source
@[simp, norm_cast]
theorem real.angle.coe_nat_mul_eq_nsmul (x : ℝ) (n : ℕ) :
↑(↑n) * x = n • ↑x
source
@[simp, norm_cast]
theorem real.angle.coe_int_mul_eq_zsmul (x : ℝ) (n : ℤ) :
↑(↑n) * x = n • ↑x
source
theorem real.angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} :
↑θ = ↑ψ ↔ ∃ (k : ℤ), θ - ψ = (2 * real.pi) * ↑k
source
@[simp]
theorem real.angle.coe_two_pi  :
↑2 * real.pi = 0
source
@[simp]
theorem real.angle.neg_coe_pi  :
-↑real.pi = ↑real.pi
source
theorem real.angle.sub_coe_pi_eq_add_coe_pi (θ : real.angle) :
θ - ↑real.pi = θ + ↑real.pi
source
@[simp]
theorem real.angle.two_nsmul_coe_pi  :
2 • ↑real.pi = 0
source
@[simp]
theorem real.angle.two_zsmul_coe_pi  :
2 • ↑real.pi = 0
source
theorem real.angle.cos_eq_iff_eq_or_eq_neg {θ ψ : ℝ} :
real.cos θ = real.cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
source
theorem real.angle.sin_eq_iff_eq_or_add_eq_pi {θ ψ : ℝ} :
real.sin θ = real.sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑real.pi
source
theorem real.angle.cos_sin_inj {θ ψ : ℝ} (Hcos : real.cos θ = real.cos ψ) (Hsin : real.sin θ = real.sin ψ) :
↑θ = ↑ψ