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
ℝ → angle as an additive homomorphism.
An induction principle to deduce results for
angle from those for
ℝ, used with
induction θ using real.angle.induction_on.