# 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.natCast_mul_eq_nsmul (x : ) (n : ) :
(n * x) = n x
@[simp]
theorem Real.Angle.intCast_mul_eq_zsmul (x : ) (n : ) :
(n * x) = n x
@[deprecated Real.Angle.natCast_mul_eq_nsmul]
theorem Real.Angle.coe_nat_mul_eq_nsmul (x : ) (n : ) :
(n * x) = n x

Alias of Real.Angle.natCast_mul_eq_nsmul.

@[deprecated Real.Angle.intCast_mul_eq_zsmul]
theorem Real.Angle.coe_int_mul_eq_zsmul (x : ) (n : ) :
(n * x) = n x

Alias of Real.Angle.intCast_mul_eq_zsmul.

theorem Real.Angle.angle_eq_iff_two_pi_dvd_sub {ψ : } {θ : } :
θ = ψ ∃ (k : ), θ - ψ = * k
@[simp]
theorem Real.Angle.coe_two_pi :
(2 * Real.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 z.natAbs), ψ = θ + 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 θ = θ = (Real.pi / 2) θ = ( / 2)
theorem Real.Angle.two_zsmul_eq_pi_iff {θ : Real.Angle} :
2 θ = θ = (Real.pi / 2) θ = ( / 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 : ) :
(↑x).sin =

The cosine of a Real.Angle.

Equations
Instances For
@[simp]
theorem Real.Angle.cos_coe (x : ) :
(↑x).cos =
theorem Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg {θ : Real.Angle} {ψ : } :
θ.cos = θ = ψ θ = -ψ
theorem Real.Angle.cos_eq_iff_eq_or_eq_neg {θ : Real.Angle} {ψ : Real.Angle} :
θ.cos = ψ.cos θ = ψ θ = -ψ
theorem Real.Angle.sin_eq_real_sin_iff_eq_or_add_eq_pi {θ : Real.Angle} {ψ : } :
θ.sin = θ = ψ θ + ψ =
theorem Real.Angle.sin_eq_iff_eq_or_add_eq_pi {θ : Real.Angle} {ψ : Real.Angle} :
θ.sin = ψ.sin θ = ψ θ + ψ =
@[simp]
theorem Real.Angle.sin_eq_zero_iff {θ : Real.Angle} :
θ.sin = 0 θ = 0 θ =
theorem Real.Angle.sin_ne_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) :
(θ + ).sin = -θ.sin
@[simp]
theorem Real.Angle.sin_sub_pi (θ : Real.Angle) :
(θ - ).sin = -θ.sin
@[simp]
@[simp]
theorem Real.Angle.cos_neg (θ : Real.Angle) :
(-θ).cos = θ.cos
@[simp]
theorem Real.Angle.cos_add_pi (θ : Real.Angle) :
(θ + ).cos = -θ.cos
@[simp]
theorem Real.Angle.cos_sub_pi (θ : Real.Angle) :
(θ - ).cos = -θ.cos
theorem Real.Angle.cos_eq_zero_iff {θ : Real.Angle} :
θ.cos = 0 θ = (Real.pi / 2) θ = ( / 2)
theorem Real.Angle.sin_add (θ₁ : Real.Angle) (θ₂ : Real.Angle) :
(θ₁ + θ₂).sin = θ₁.sin * θ₂.cos + θ₁.cos * θ₂.sin
theorem Real.Angle.cos_add (θ₁ : Real.Angle) (θ₂ : 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.sin_add_pi_div_two (θ : Real.Angle) :
(θ + (Real.pi / 2)).sin = θ.cos
theorem Real.Angle.sin_sub_pi_div_two (θ : Real.Angle) :
(θ - (Real.pi / 2)).sin = -θ.cos
theorem Real.Angle.sin_pi_div_two_sub (θ : Real.Angle) :
((Real.pi / 2) - θ).sin = θ.cos
theorem Real.Angle.cos_add_pi_div_two (θ : Real.Angle) :
(θ + (Real.pi / 2)).cos = -θ.sin
theorem Real.Angle.cos_sub_pi_div_two (θ : Real.Angle) :
(θ - (Real.pi / 2)).cos = θ.sin
theorem Real.Angle.cos_pi_div_two_sub (θ : Real.Angle) :
((Real.pi / 2) - θ).cos = θ.sin
theorem Real.Angle.abs_sin_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
|θ.sin| = |ψ.sin|
theorem Real.Angle.abs_sin_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
|θ.sin| = |ψ.sin|
theorem Real.Angle.abs_cos_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
|θ.cos| = |ψ.cos|
theorem Real.Angle.abs_cos_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
|θ.cos| = |ψ.cos|
@[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
• θ.toReal =
Instances For
theorem Real.Angle.toReal_coe (θ : ) :
(↑θ).toReal =
theorem Real.Angle.toReal_coe_eq_self_iff {θ : } :
(↑θ).toReal = θ
theorem Real.Angle.toReal_coe_eq_self_iff_mem_Ioc {θ : } :
(↑θ).toReal = θ
@[simp]
theorem Real.Angle.toReal_inj {θ : Real.Angle} {ψ : Real.Angle} :
θ.toReal = ψ.toReal θ = ψ
@[simp]
theorem Real.Angle.coe_toReal (θ : Real.Angle) :
θ.toReal = θ
@[simp]
@[simp]
theorem Real.Angle.toReal_eq_zero_iff {θ : Real.Angle} :
θ.toReal = 0 θ = 0
@[simp]
theorem Real.Angle.toReal_pi :
(↑Real.pi).toReal = Real.pi
@[simp]
theorem Real.Angle.toReal_eq_pi_iff {θ : Real.Angle} :
θ.toReal = Real.pi θ =
@[simp]
theorem Real.Angle.toReal_pi_div_two :
(↑(Real.pi / 2)).toReal =
@[simp]
theorem Real.Angle.toReal_eq_pi_div_two_iff {θ : Real.Angle} :
θ.toReal = θ = (Real.pi / 2)
@[simp]
theorem Real.Angle.toReal_neg_pi_div_two :
(↑( / 2)).toReal =
@[simp]
theorem Real.Angle.toReal_eq_neg_pi_div_two_iff {θ : Real.Angle} :
θ.toReal = θ = ( / 2)
theorem Real.Angle.abs_toReal_coe_eq_self_iff {θ : } :
|(↑θ).toReal| = θ 0 θ
theorem Real.Angle.abs_toReal_neg_coe_eq_self_iff {θ : } :
|(-θ).toReal| = θ 0 θ
theorem Real.Angle.abs_toReal_eq_pi_div_two_iff {θ : Real.Angle} :
|θ.toReal| = θ = (Real.pi / 2) θ = ( / 2)
theorem Real.Angle.nsmul_toReal_eq_mul {n : } (h : n 0) {θ : Real.Angle} :
(n θ).toReal = n * θ.toReal θ.toReal Set.Ioc ( / n) (Real.pi / n)
theorem Real.Angle.two_nsmul_toReal_eq_two_mul {θ : Real.Angle} :
(2 θ).toReal = 2 * θ.toReal θ.toReal Set.Ioc ( / 2) (Real.pi / 2)
theorem Real.Angle.two_zsmul_toReal_eq_two_mul {θ : Real.Angle} :
(2 θ).toReal = 2 * θ.toReal θ.toReal Set.Ioc ( / 2) (Real.pi / 2)
theorem Real.Angle.toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff {θ : } {k : } :
(↑θ).toReal = θ - 2 * k * Real.pi θ Set.Ioc ((2 * k - 1) * Real.pi) ((2 * k + 1) * Real.pi)
theorem Real.Angle.toReal_coe_eq_self_sub_two_pi_iff {θ : } :
(↑θ).toReal = θ - θ
theorem Real.Angle.two_nsmul_toReal_eq_two_mul_sub_two_pi {θ : Real.Angle} :
(2 θ).toReal = 2 * θ.toReal - < θ.toReal
theorem Real.Angle.two_zsmul_toReal_eq_two_mul_sub_two_pi {θ : Real.Angle} :
(2 θ).toReal = 2 * θ.toReal - < θ.toReal
theorem Real.Angle.two_nsmul_toReal_eq_two_mul_add_two_pi {θ : Real.Angle} :
(2 θ).toReal = 2 * θ.toReal + θ.toReal
theorem Real.Angle.two_zsmul_toReal_eq_two_mul_add_two_pi {θ : Real.Angle} :
(2 θ).toReal = 2 * θ.toReal + θ.toReal
@[simp]
theorem Real.Angle.sin_toReal (θ : Real.Angle) :
Real.sin θ.toReal = θ.sin
@[simp]
theorem Real.Angle.cos_toReal (θ : Real.Angle) :
Real.cos θ.toReal = θ.cos
theorem Real.Angle.abs_cos_eq_abs_sin_of_two_nsmul_add_two_nsmul_eq_pi {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ + 2 ψ = ) :
|θ.cos| = |ψ.sin|
theorem Real.Angle.abs_cos_eq_abs_sin_of_two_zsmul_add_two_zsmul_eq_pi {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ + 2 ψ = ) :
|θ.cos| = |ψ.sin|

The tangent of a Real.Angle.

Equations
• θ.tan = θ.sin / θ.cos
Instances For
theorem Real.Angle.tan_eq_sin_div_cos (θ : Real.Angle) :
θ.tan = θ.sin / θ.cos
@[simp]
theorem Real.Angle.tan_coe (x : ) :
(↑x).tan =
@[simp]
@[simp]
theorem Real.Angle.tan_add_pi (θ : Real.Angle) :
(θ + ).tan = θ.tan
@[simp]
theorem Real.Angle.tan_sub_pi (θ : Real.Angle) :
(θ - ).tan = θ.tan
@[simp]
theorem Real.Angle.tan_toReal (θ : Real.Angle) :
Real.tan θ.toReal = θ.tan
theorem Real.Angle.tan_eq_of_two_nsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
θ.tan = ψ.tan
theorem Real.Angle.tan_eq_of_two_zsmul_eq {θ : Real.Angle} {ψ : Real.Angle} (h : 2 θ = 2 ψ) :
θ.tan = ψ.tan

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
• θ.sign = SignType.sign θ.sin
Instances For
@[simp]
@[simp]
theorem Real.Angle.sign_coe_pi :
(↑Real.pi).sign = 0
@[simp]
theorem Real.Angle.sign_neg (θ : Real.Angle) :
(-θ).sign = -θ.sign
@[simp]
theorem Real.Angle.sign_add_pi (θ : Real.Angle) :
(θ + ).sign = -θ.sign
@[simp]
theorem Real.Angle.sign_pi_add (θ : Real.Angle) :
( + θ).sign = -θ.sign
@[simp]
theorem Real.Angle.sign_sub_pi (θ : Real.Angle) :
(θ - ).sign = -θ.sign
@[simp]
theorem Real.Angle.sign_pi_sub (θ : Real.Angle) :
( - θ).sign = θ.sign
theorem Real.Angle.sign_eq_zero_iff {θ : Real.Angle} :
θ.sign = 0 θ = 0 θ =
theorem Real.Angle.sign_ne_zero_iff {θ : Real.Angle} :
θ.sign 0 θ 0 θ
theorem Real.Angle.toReal_neg_iff_sign_neg {θ : Real.Angle} :
θ.toReal < 0 θ.sign = -1
@[simp]
theorem Real.Angle.sign_toReal {θ : Real.Angle} (h : θ ) :
SignType.sign θ.toReal = θ.sign
theorem Real.Angle.coe_abs_toReal_of_sign_nonneg {θ : Real.Angle} (h : 0 θ.sign) :
|θ.toReal| = θ
theorem Real.Angle.neg_coe_abs_toReal_of_sign_nonpos {θ : Real.Angle} (h : θ.sign 0) :
-|θ.toReal| = θ
theorem Real.Angle.eq_iff_sign_eq_and_abs_toReal_eq {θ : Real.Angle} {ψ : Real.Angle} :
θ = ψ θ.sign = ψ.sign |θ.toReal| = |ψ.toReal|
theorem Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq {θ : Real.Angle} {ψ : Real.Angle} (h : θ.sign = ψ.sign) :
θ = ψ |θ.toReal| = |ψ.toReal|
@[simp]
theorem Real.Angle.sign_coe_pi_div_two :
(↑(Real.pi / 2)).sign = 1
@[simp]
theorem Real.Angle.sign_coe_neg_pi_div_two :
(↑( / 2)).sign = -1
theorem Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi {θ : } (h0 : 0 θ) (hpi : ) :
0 (↑θ).sign
theorem Real.Angle.sign_neg_coe_nonpos_of_nonneg_of_le_pi {θ : } (h0 : 0 θ) (hpi : ) :
(-θ).sign 0
theorem Real.Angle.sign_two_nsmul_eq_sign_iff {θ : Real.Angle} :
(2 θ).sign = θ.sign θ = |θ.toReal| <
theorem Real.Angle.sign_two_zsmul_eq_sign_iff {θ : Real.Angle} :
(2 θ).sign = θ.sign θ = |θ.toReal| <
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) :
(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.