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 canonical map from ℝ
to the quotient Angle
.
Instances For
Coercion ℝ → Angle
as an additive homomorphism.
Instances For
An induction principle to deduce results for Angle
from those for ℝ
, used with
induction θ using Real.Angle.induction_on
.
Convert a Real.Angle
to a real number in the interval Ioc (-π) π
.
Instances For
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.
Instances For
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.