The additive circle is infinite #
For a positive period p in a densely ordered archimedean group, AddCircle p is in bijection
with the half-open interval [0, p) (AddCircle.equivIco), which is infinite. In particular the
unit circle UnitAddCircle is infinite.
Main results #
AddCircle.infinite:AddCircle pis infinite, as an instance.
instance
AddCircle.infinite
{𝕜 : Type u_1}
[AddCommGroup 𝕜]
[LinearOrder 𝕜]
[IsOrderedAddMonoid 𝕜]
[Archimedean 𝕜]
[DenselyOrdered 𝕜]
{p : 𝕜}
[Fact (0 < p)]
:
The additive circle of a positive period in a densely ordered archimedean group is infinite,
being in bijection with the interval [0, p).