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]
The type of angles
Equations
- real.angle = (ℝ ⧸ add_subgroup.zmultiples (2 * real.pi))
@[protected, instance]
Equations
- real.angle.inhabited = {default := 0}
@[protected, instance]
Equations
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
.
The sine of a real.angle
.
Equations
- θ.sin = real.sin_periodic.lift θ
The cosine of a real.angle
.
Equations
- θ.cos = real.cos_periodic.lift θ