# 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.

The type of angles

Equations
Instances For
Equations

The canonical map from ℝ to the quotient Angle.

Equations
• r = r
Instances For
Equations

Coercion ℝ → Angle as an additive homomorphism.

Equations
Instances For
@[simp]
theorem Real.Angle.induction_on {p : } (θ : 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 : ) :
(-x) = -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]
theorem Real.Angle.coe_nat_mul_eq_nsmul (x : ) (n : ) :
(n * x) = n x
@[simp]
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 :
() = 0
@[simp]
@[simp]
theorem Real.Angle.two_nsmul_coe_div_two (θ : ) :
2 (θ / 2) = θ
@[simp]
theorem Real.Angle.two_zsmul_coe_div_two (θ : ) :
2 (θ / 2) = θ
theorem Real.Angle.zsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} {z : } (hz : z 0) :
z ψ = z θ ∃ (k : Fin ()), ψ = θ + k ( / z)
theorem Real.Angle.nsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} {n : } (hz : n 0) :
n ψ = n θ ∃ (k : Fin n), ψ = θ + k ( / n)
theorem Real.Angle.two_zsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} :
2 ψ = 2 θ ψ = θ ψ = θ +
theorem Real.Angle.two_nsmul_eq_iff {ψ : Real.Angle} {θ : Real.Angle} :
2 ψ = 2 θ ψ = θ ψ = θ +
theorem Real.Angle.eq_neg_self_iff {θ : Real.Angle} :
θ = -θ θ = 0 θ =
theorem Real.Angle.neg_eq_self_iff {θ : Real.Angle} :
-θ = θ θ = 0 θ =
theorem Real.Angle.two_nsmul_eq_pi_iff {θ : Real.Angle} :
2 θ = θ = () θ = ()
theorem Real.Angle.two_zsmul_eq_pi_iff {θ : Real.Angle} :
2 θ = θ = () θ = ()
theorem Real.Angle.cos_eq_iff_coe_eq_or_eq_neg {θ : } {ψ : } :
θ = ψ θ = -ψ
theorem Real.Angle.sin_eq_iff_coe_eq_or_add_eq_pi {θ : } {ψ : } :
θ = ψ θ + ψ =
theorem Real.Angle.cos_sin_inj {θ : } {ψ : } (Hcos : ) (Hsin : ) :
θ = ψ

The sine of a Real.Angle.

Equations
Instances For
@[simp]
theorem Real.Angle.sin_coe (x : ) :

The cosine of a Real.Angle.

Equations
Instances For
@[simp]
theorem Real.Angle.cos_coe (x : ) :
theorem Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg {θ : Real.Angle} {ψ : } :
θ = ψ θ = -ψ
theorem Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi {θ : Real.Angle} {ψ : } :
θ = ψ θ + ψ =
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem Real.Angle.cos_eq_zero_iff {θ : Real.Angle} :
θ = () θ = ()
theorem Real.Angle.sin_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) :
Real.Angle.sin (θ₁ + θ₂) = +
theorem Real.Angle.cos_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) :
Real.Angle.cos (θ₁ + θ₂) = -
theorem Real.Angle.abs_sin_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
|| = ||
theorem Real.Angle.abs_sin_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
|| = ||
theorem Real.Angle.abs_cos_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
|| = ||
theorem Real.Angle.abs_cos_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
|| = ||
@[simp]
theorem Real.Angle.coe_toIcoMod (θ : ) (ψ : ) :
() = θ
@[simp]
theorem Real.Angle.coe_toIocMod (θ : ) (ψ : ) :
() = θ

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

Equations
Instances For
@[simp]
theorem Real.Angle.toReal_inj {θ : Real.Angle} {ψ : Real.Angle} :
θ = ψ
@[simp]
theorem Real.Angle.coe_toReal (θ : Real.Angle) :
= θ
@[simp]
@[simp]
@[simp]
theorem Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : } {k : } :
= θ - 2 * k * Real.pi θ Set.Ioc ((2 * k - 1) * Real.pi) ((2 * k + 1) * Real.pi)
@[simp]
@[simp]

The tangent of a Real.Angle.

Equations
Instances For
@[simp]
theorem Real.Angle.tan_coe (x : ) :
@[simp]
@[simp]
@[simp]
@[simp]
theorem Real.Angle.tan_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
theorem Real.Angle.tan_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :

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
• = SignType.sign ()
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem Real.Angle.sign_toReal {θ : Real.Angle} (h : θ ) :
SignType.sign =
theorem Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi {θ : } (h0 : 0 θ) (hpi : ) :
0
theorem Real.Angle.continuousAt_sign {θ : Real.Angle} (h0 : θ 0) (hpi : θ ) :
theorem ContinuousOn.angle_sign_comp {α : Type u_1} [] {f : } {s : Set α} (hf : ) (hs : zs, f z 0 f z ) :
theorem Real.Angle.sign_eq_of_continuousOn {α : Type u_1} [] {f : } {s : Set α} {x : α} {y : α} (hc : ) (hf : ) (hs : zs, f z 0 f z ) (hx : x s) (hy : y s) :

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.