# mathlib3documentation

analysis.special_functions.trigonometric.angle

# The type of angles #

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

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]
noncomputable def real.angle.inhabited  :
@[protected, instance]
noncomputable def real.angle.has_coe_t  :
@[protected, instance]
def real.angle  :

The type of angles

Equations
Instances for real.angle
@[protected, instance]
noncomputable def real.angle.circular_order  :
Equations
@[continuity]
noncomputable def real.angle.coe_hom  :

Coercion ℝ → angle as an additive homomorphism.

Equations
@[simp]
@[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
theorem real.angle.coe_nsmul (n : ) (x : ) :
(n x) = n x
theorem real.angle.coe_zsmul (z : ) (x : ) :
(z x) = z x
@[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 : ), θ - ψ = * k
@[simp]
theorem real.angle.coe_two_pi  :
(2 * real.pi) = 0
@[simp]
theorem real.angle.neg_coe_pi  :
@[simp]
theorem real.angle.two_nsmul_coe_div_two (θ : ) :
2 / 2) = θ
@[simp]
theorem real.angle.two_zsmul_coe_div_two (θ : ) :
2 / 2) = θ
@[simp]
@[simp]
@[simp]
theorem real.angle.zsmul_eq_iff {ψ θ : real.angle} {z : } (hz : z 0) :
z ψ = z θ (k : fin z.nat_abs), ψ = θ + k (2 * real.pi / z)
theorem real.angle.nsmul_eq_iff {ψ θ : real.angle} {n : } (hz : n 0) :
n ψ = n θ (k : fin n), ψ = θ + k (2 * real.pi / n)
theorem real.angle.two_zsmul_eq_iff {ψ θ : real.angle} :
2 ψ = 2 θ ψ = θ ψ =
theorem real.angle.two_nsmul_eq_iff {ψ θ : real.angle} :
2 ψ = 2 θ ψ = θ ψ =
theorem real.angle.eq_neg_self_iff {θ : real.angle} :
θ = -θ θ = 0
theorem real.angle.ne_neg_self_iff {θ : real.angle} :
θ -θ θ 0
theorem real.angle.neg_eq_self_iff {θ : real.angle} :
-θ = θ θ = 0
theorem real.angle.neg_ne_self_iff {θ : real.angle} :
-θ θ θ 0
theorem real.angle.cos_sin_inj {θ ψ : } (Hcos : = ) (Hsin : = ) :
θ = ψ
noncomputable def real.angle.sin (θ : real.angle) :

The sine of a real.angle.

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

The cosine of a real.angle.

Equations
@[simp]
theorem real.angle.cos_coe (x : ) :
@[continuity]
theorem real.angle.cos_eq_iff_eq_or_eq_neg {θ ψ : real.angle} :
θ.cos = ψ.cos θ = ψ θ = -ψ
@[simp]
theorem real.angle.sin_zero  :
0.sin = 0
@[simp]
theorem real.angle.sin_coe_pi  :
theorem real.angle.sin_eq_zero_iff {θ : real.angle} :
θ.sin = 0 θ = 0
@[simp]
theorem real.angle.sin_neg (θ : real.angle) :
(-θ).sin = -θ.sin
@[simp]
theorem real.angle.sin_add_pi (θ : real.angle) :
@[simp]
theorem real.angle.sin_sub_pi (θ : real.angle) :
@[simp]
theorem real.angle.cos_zero  :
0.cos = 1
@[simp]
@[simp]
theorem real.angle.cos_neg (θ : real.angle) :
(-θ).cos = θ.cos
@[simp]
theorem real.angle.cos_add_pi (θ : real.angle) :
@[simp]
theorem real.angle.cos_sub_pi (θ : real.angle) :
theorem real.angle.sin_add (θ₁ θ₂ : real.angle) :
(θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
theorem real.angle.cos_add (θ₁ θ₂ : real.angle) :
(θ₁ + θ₂).cos = θ₁.cos * θ₂.cos - θ₁.sin * θ₂.sin
@[simp]
theorem real.angle.cos_sq_add_sin_sq (θ : real.angle) :
θ.cos ^ 2 + θ.sin ^ 2 = 1
theorem real.angle.abs_sin_eq_of_two_nsmul_eq {θ ψ : real.angle} (h : 2 θ = 2 ψ) :
|θ.sin| = |ψ.sin|
theorem real.angle.abs_sin_eq_of_two_zsmul_eq {θ ψ : real.angle} (h : 2 θ = 2 ψ) :
|θ.sin| = |ψ.sin|
theorem real.angle.abs_cos_eq_of_two_nsmul_eq {θ ψ : real.angle} (h : 2 θ = 2 ψ) :
|θ.cos| = |ψ.cos|
theorem real.angle.abs_cos_eq_of_two_zsmul_eq {θ ψ : real.angle} (h : 2 θ = 2 ψ) :
|θ.cos| = |ψ.cos|
@[simp]
theorem real.angle.coe_to_Ico_mod (θ ψ : ) :
@[simp]
theorem real.angle.coe_to_Ioc_mod (θ ψ : ) :
noncomputable def real.angle.to_real (θ : real.angle) :

Convert a real.angle to a real number in the interval Ioc (-π) π.

Equations
theorem real.angle.to_real_coe (θ : ) :
@[simp]
theorem real.angle.to_real_inj {θ ψ : real.angle} :
θ.to_real = ψ.to_real θ = ψ
@[simp]
theorem real.angle.coe_to_real (θ : real.angle) :
(θ.to_real) = θ
@[simp]
@[simp]
@[simp]
theorem real.angle.to_real_eq_zero_iff {θ : real.angle} :
θ.to_real = 0 θ = 0
@[simp]
theorem real.angle.to_real_pi  :
@[simp]
theorem real.angle.sin_to_real (θ : real.angle) :
= θ.sin
@[simp]
theorem real.angle.cos_to_real (θ : real.angle) :
= θ.cos
noncomputable def real.angle.tan (θ : real.angle) :

The tangent of a real.angle.

Equations
@[simp]
theorem real.angle.tan_coe (x : ) :
@[simp]
theorem real.angle.tan_zero  :
0.tan = 0
@[simp]
theorem real.angle.tan_coe_pi  :
@[simp]
theorem real.angle.tan_add_pi (θ : real.angle) :
+ real.pi).tan = θ.tan
@[simp]
theorem real.angle.tan_sub_pi (θ : real.angle) :
- real.pi).tan = θ.tan
@[simp]
theorem real.angle.tan_to_real (θ : real.angle) :
= θ.tan
theorem real.angle.tan_eq_of_two_nsmul_eq {θ ψ : real.angle} (h : 2 θ = 2 ψ) :
θ.tan = ψ.tan
theorem real.angle.tan_eq_of_two_zsmul_eq {θ ψ : real.angle} (h : 2 θ = 2 ψ) :
θ.tan = ψ.tan
noncomputable def real.angle.sign (θ : real.angle) :

The sign of a real.angle is 0 if the angle is 0 or π, 1 if the angle is strictly between 0 and π and -1 is the angle is strictly between -π and 0. It is defined as the sign of the sine of the angle.

Equations
@[simp]
theorem real.angle.sign_zero  :
0.sign = 0
@[simp]
@[simp]
theorem real.angle.sign_neg (θ : real.angle) :
(-θ).sign = -θ.sign
@[simp]
@[simp]
@[simp]
@[simp]
theorem real.angle.sign_eq_zero_iff {θ : real.angle} :
θ.sign = 0 θ = 0
@[simp]
theorem real.angle.sign_to_real {θ : real.angle} (h : θ real.pi) :
= θ.sign
theorem real.angle.eq_iff_abs_to_real_eq_of_sign_eq {θ ψ : real.angle} (h : θ.sign = ψ.sign) :
θ = ψ
theorem real.angle.sign_coe_nonneg_of_nonneg_of_le_pi {θ : } (h0 : 0 θ) (hpi : θ real.pi) :
theorem real.angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi {θ : } (h0 : 0 θ) (hpi : θ real.pi) :
(-θ).sign 0
theorem real.angle.continuous_at_sign {θ : real.angle} (h0 : θ 0) (hpi : θ real.pi) :
theorem continuous_on.angle_sign_comp {α : Type u_1} {f : α real.angle} {s : set α} (hf : s) (hs : (z : α), z s f z 0 f z real.pi) :
theorem real.angle.sign_eq_of_continuous_on {α : Type u_1} {f : α real.angle} {s : set α} {x y : α} (hc : is_connected s) (hf : s) (hs : (z : α), z s f z 0 f z real.pi) (hx : x s) (hy : y s) :
(f y).sign = (f x).sign

Suppose a function to angles is continuous on a connected set and never takes the values 0 or π on that set. Then the values of the function on that set all have the same sign.