# mathlib3documentation

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the additive circle add_circle p as the quotient π β§Έ (β€ β p) for some period p : π.

See also circle and real.angle. For the normed group structure on add_circle, see add_circle.normed_add_comm_group in a later file.

## Main definitions and results: #

• add_circle: the additive circle π β§Έ (β€ β p) for some period p : π
• unit_add_circle: the special case β β§Έ β€
• add_circle.equiv_add_circle: the rescaling equivalence add_circle p β+ add_circle q
• add_circle.equiv_Ico: the natural equivalence add_circle p β Ico a (a + p)
• add_circle.add_order_of_div_of_gcd_eq_one: rational points have finite order
• add_circle.exists_gcd_eq_one_of_is_of_fin_add_order: finite-order points are rational
• add_circle.homeo_Icc_quot: the natural topological equivalence between add_circle p and Icc a (a + p) with its endpoints identified.
• add_circle.lift_Ico_continuous: if f : β β B is continuous, and f a = f (a + p) for some a, then there is a continuous function add_circle p β B which agrees with f on Icc a (a + p).

## Implementation notes: #

Although the most important case is π = β we wish to support other types of scalars, such as the rational circle add_circle (1 : β), and so we set things up more generally.

## TODO #

• Lie group structure
• Exponential equivalence to circle
theorem continuous_right_to_Ico_mod {π : Type u_1} [archimedean π] [topological_space π] [order_topology π] {p : π} (hp : 0 < p) (a x : π) :
(set.Ici x) x
theorem continuous_left_to_Ioc_mod {π : Type u_1} [archimedean π] [topological_space π] [order_topology π] {p : π} (hp : 0 < p) (a x : π) :
(set.Iic x) x
theorem to_Ico_mod_eventually_eq_to_Ioc_mod {π : Type u_1} [archimedean π] [topological_space π] [order_topology π] {p : π} (hp : 0 < p) (a : π) {x : π} (hx : βx β  βa) :
theorem continuous_at_to_Ico_mod {π : Type u_1} [archimedean π] [topological_space π] [order_topology π] {p : π} (hp : 0 < p) (a : π) {x : π} (hx : βx β  βa) :
theorem continuous_at_to_Ioc_mod {π : Type u_1} [archimedean π] [topological_space π] [order_topology π] {p : π} (hp : 0 < p) (a : π) {x : π} (hx : βx β  βa) :
@[protected, instance]
def add_circle.add_comm_group {π : Type u_1} [topological_space π] [order_topology π] (p : π) :
@[nolint]
def add_circle {π : Type u_1} [topological_space π] [order_topology π] (p : π) :
Type u_1

The "additive circle": π β§Έ (β€ β p). See also circle and real.angle.

Equations
Instances for add_circle
@[protected, instance]
def add_circle.topological_space {π : Type u_1} [topological_space π] [order_topology π] (p : π) :
@[protected, instance]
def add_circle.has_coe_t {π : Type u_1} [topological_space π] [order_topology π] (p : π) :
@[protected, instance]
def add_circle.inhabited {π : Type u_1} [topological_space π] [order_topology π] (p : π) :
@[protected, instance]
def add_circle.topological_add_group {π : Type u_1} [topological_space π] [order_topology π] (p : π) :
theorem add_circle.coe_nsmul {π : Type u_1} [topological_space π] [order_topology π] (p : π) {n : β} {x : π} :
theorem add_circle.coe_zsmul {π : Type u_1} [topological_space π] [order_topology π] (p : π) {n : β€} {x : π} :
theorem add_circle.coe_add {π : Type u_1} [topological_space π] [order_topology π] (p x y : π) :
theorem add_circle.coe_sub {π : Type u_1} [topological_space π] [order_topology π] (p x y : π) :
theorem add_circle.coe_neg {π : Type u_1} [topological_space π] [order_topology π] (p : π) {x : π} :
theorem add_circle.coe_eq_zero_iff {π : Type u_1} [topological_space π] [order_topology π] (p : π) {x : π} :
theorem add_circle.coe_eq_zero_of_pos_iff {π : Type u_1} [topological_space π] [order_topology π] (p : π) (hp : 0 < p) {x : π} (hx : 0 < x) :
theorem add_circle.coe_period {π : Type u_1} [topological_space π] [order_topology π] (p : π) :
@[simp]
theorem add_circle.coe_add_period {π : Type u_1} [topological_space π] [order_topology π] (p x : π) :
@[protected, nolint, continuity]
theorem add_circle.continuous_mk' {π : Type u_1} [topological_space π] [order_topology π] (p : π) :
@[protected, instance]
def add_circle.circular_order {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] [archimedean π] :
Equations
noncomputable def add_circle.equiv_Ico {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] :

The equivalence between add_circle p and the half-open interval [a, a + p), whose inverse is the natural quotient map.

Equations
noncomputable def add_circle.equiv_Ioc {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] :

The equivalence between add_circle p and the half-open interval (a, a + p], whose inverse is the natural quotient map.

Equations
noncomputable def add_circle.lift_Ico {π : Type u_1} {B : Type u_2} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] (f : π β B) :

Given a function on π, return the unique function on add_circle p agreeing with f on [a, a + p).

Equations
noncomputable def add_circle.lift_Ioc {π : Type u_1} {B : Type u_2} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] (f : π β B) :

Given a function on π, return the unique function on add_circle p agreeing with f on (a, a + p].

Equations
theorem add_circle.coe_eq_coe_iff_of_mem_Ico {π : Type u_1} [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {a : π} [archimedean π] {x y : π} (hx : x β (a + p)) (hy : y β (a + p)) :
theorem add_circle.lift_Ico_coe_apply {π : Type u_1} {B : Type u_2} [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {a : π} [archimedean π] {f : π β B} {x : π} (hx : x β (a + p)) :
f βx = f x
theorem add_circle.lift_Ioc_coe_apply {π : Type u_1} {B : Type u_2} [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {a : π} [archimedean π] {f : π β B} {x : π} (hx : x β (a + p)) :
f βx = f x
@[continuity]
theorem add_circle.continuous_equiv_Ico_symm {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] :
@[continuity]
theorem add_circle.continuous_equiv_Ioc_symm {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] :
theorem add_circle.continuous_at_equiv_Ico {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] {x : add_circle p} (hx : x β  βa) :
theorem add_circle.continuous_at_equiv_Ioc {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] {x : add_circle p} (hx : x β  βa) :
@[simp]
theorem add_circle.coe_image_Ico_eq {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] :
coe '' (a + p) = set.univ

The image of the closed-open interval [a, a + p) under the quotient map π β add_circle p is the entire space.

@[simp]
theorem add_circle.coe_image_Ioc_eq {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] :
coe '' (a + p) = set.univ

The image of the closed-open interval [a, a + p) under the quotient map π β add_circle p is the entire space.

@[simp]
theorem add_circle.coe_image_Icc_eq {π : Type u_1} [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] (a : π) [archimedean π] :
coe '' (a + p) = set.univ

The image of the closed interval [0, p] under the quotient map π β add_circle p is the entire space.

def add_circle.equiv_add_circle {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p q : π) (hp : p β  0) (hq : q β  0) :

The rescaling equivalence between additive circles with different periods.

Equations
@[simp]
theorem add_circle.equiv_add_circle_apply_mk {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p q : π) (hp : p β  0) (hq : q β  0) (x : π) :
β hp hq) βx = β(x * (pβ»ΒΉ * q))
@[simp]
theorem add_circle.equiv_add_circle_symm_apply_mk {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p q : π) (hp : p β  0) (hq : q β  0) (x : π) :
β hp hq).symm) βx = β(x * (qβ»ΒΉ * p))
@[simp]
theorem add_circle.coe_equiv_Ico_mk_apply {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] [floor_ring π] (x : π) :
β(β 0) = int.fract (x / p) * p
@[protected, instance]
noncomputable def add_circle.int.divisible_by {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] [floor_ring π] :
Equations
theorem add_circle.add_order_of_period_div {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {n : β} (h : 0 < n) :
theorem add_circle.gcd_mul_add_order_of_div_eq {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] {n : β} (m : β) (hn : 0 < n) :
theorem add_circle.add_order_of_div_of_gcd_eq_one {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {m n : β} (hn : 0 < n) (h : m.gcd n = 1) :
theorem add_circle.add_order_of_div_of_gcd_eq_one' {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {m : β€} {n : β} (hn : 0 < n) (h : m.nat_abs.gcd n = 1) :
theorem add_circle.add_order_of_coe_rat {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {q : β} :
theorem add_circle.add_order_of_eq_pos_iff {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {u : add_circle p} {n : β} (h : 0 < n) :
β β (m : β) (H : m < n), m.gcd n = 1 β§ β(βm / βn * p) = u
theorem add_circle.exists_gcd_eq_one_of_is_of_fin_add_order {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] {u : add_circle p} (h : is_of_fin_add_order u) :
noncomputable def add_circle.set_add_order_of_equiv {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] {n : β} (hn : 0 < n) :
β₯{u : | = n} β β₯{m : β | m < n β§ m.gcd n = 1}

The natural bijection between points of order n and natural numbers less than and coprime to n. The inverse of the map sends m β¦ (m/n * p : add_circle p) where m is coprime to n and satisfies 0 β€ m < n.

Equations
@[simp]
theorem add_circle.card_add_order_of_eq_totient {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] {n : β} :
nat.card {u // = n} = n.totient
theorem add_circle.finite_set_of_add_order_eq {π : Type u_1} [linear_ordered_field π] [topological_space π] [order_topology π] (p : π) [hp : fact (0 < p)] {n : β} (hn : 0 < n) :
{u : | = n}.finite
@[protected, instance]
def add_circle.compact_space (p : β) [fact (0 < p)] :

The "additive circle" β β§Έ (β€ β p) is compact.

@[protected, instance]

The action on β by right multiplication of its the subgroup zmultiples p (the multiples of p:β) is properly discontinuous.

@[protected, instance]

The "additive circle" β β§Έ (β€ β p) is Hausdorff.

@[protected, instance]
def add_circle.normal_space (p : β) [fact (0 < p)] :

The "additive circle" β β§Έ (β€ β p) is normal.

@[protected, instance]

The "additive circle" β β§Έ (β€ β p) is second-countable.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[reducible]

The unit circle β β§Έ β€.

This section proves that for any a, the natural map from [a, a + p] β π to add_circle p gives an identification of add_circle p, as a topological space, with the quotient of [a, a + p] by the equivalence relation identifying the endpoints.

inductive add_circle.endpoint_ident {π : Type u_1} [topological_space π] [order_topology π] (p a : π) [hp : fact (0 < p)] :
β₯(set.Icc a (a + p)) β β₯(set.Icc a (a + p)) β Prop

The relation identifying the endpoints of Icc a (a + p).

noncomputable def add_circle.equiv_Icc_quot {π : Type u_1} [topological_space π] [order_topology π] (p a : π) [hp : fact (0 < p)] [archimedean π] :
β quot

The equivalence between add_circle p and the quotient of [a, a + p] by the relation identifying the endpoints.

Equations
theorem add_circle.equiv_Icc_quot_comp_mk_eq_to_Ico_mod {π : Type u_1} [topological_space π] [order_topology π] (p a : π) [hp : fact (0 < p)] [archimedean π] :
= Ξ» (x : π), quot.mk β¨ a x, _β©
theorem add_circle.equiv_Icc_quot_comp_mk_eq_to_Ioc_mod {π : Type u_1} [topological_space π] [order_topology π] (p a : π) [hp : fact (0 < p)] [archimedean π] :
= Ξ» (x : π), quot.mk β¨ a x, _β©
noncomputable def add_circle.homeo_Icc_quot {π : Type u_1} [topological_space π] [order_topology π] (p a : π) [hp : fact (0 < p)] [archimedean π] :

The natural map from [a, a + p] β π with endpoints identified to π / β€ β’ p, as a homeomorphism of topological spaces.

Equations

We now show that a continuous function on [a, a + p] satisfying f a = f (a + p) is the pullback of a continuous function on add_circle p.

theorem add_circle.lift_Ico_eq_lift_Icc {π : Type u_1} {B : Type u_2} [topological_space π] [order_topology π] {p a : π} [hp : fact (0 < p)] [archimedean π] {f : π β B} (h : f a = f (a + p)) :
f = quot.lift ((set.Icc a (a + p)).restrict f) _ β
theorem add_circle.lift_Ico_continuous {π : Type u_1} {B : Type u_2} [topological_space π] [order_topology π] {p a : π} [hp : fact (0 < p)] [archimedean π] {f : π β B} (hf : f a = f (a + p)) (hc : (set.Icc a (a + p))) :
theorem add_circle.lift_Ico_zero_coe_apply {π : Type u_1} {B : Type u_2} [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] [archimedean π] {f : π β B} {x : π} (hx : x β p) :
f βx = f x
theorem add_circle.lift_Ico_zero_continuous {π : Type u_1} {B : Type u_2} [topological_space π] [order_topology π] {p : π} [hp : fact (0 < p)] [archimedean π] {f : π β B} (hf : f 0 = f p) (hc : (set.Icc 0 p)) :