mathlib documentation

topology.instances.add_circle

The additive circle #

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: #

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 #

@[protected, instance]
def add_circle.add_comm_group {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
@[protected, instance]
def add_circle.topological_space {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
@[protected, instance]
def add_circle.has_coe_t {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
has_coe_t π•œ (add_circle p)
@[protected, instance]
def add_circle.inhabited {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) :
@[protected, instance]
theorem add_circle.coe_nsmul {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) {n : β„•} {x : π•œ} :
theorem add_circle.coe_zsmul {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) {n : β„€} {x : π•œ} :
theorem add_circle.coe_neg {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) {x : π•œ} :
theorem add_circle.coe_eq_zero_iff {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) {x : π•œ} :
theorem add_circle.coe_eq_zero_of_pos_iff {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) (hp : 0 < p) {x : π•œ} (hx : 0 < x) :
@[protected, nolint, continuity]
noncomputable def add_circle.equiv_Ico {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :

The natural equivalence between add_circle p and the half-open interval [0, p).

Equations
@[continuity]
theorem add_circle.continuous_equiv_Ico_symm {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :
@[simp]
theorem add_circle.coe_image_Ico_eq {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :

The image of the closed-open interval [0, p) under the quotient map π•œ β†’ add_circle p is the entire space.

@[simp]
theorem add_circle.coe_image_Icc_eq {π•œ : Type u_1} [linear_ordered_add_comm_group π•œ] [topological_space π•œ] [order_topology π•œ] (p : π•œ) [hp : fact (0 < p)] [archimedean π•œ] :

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 : π•œ) :
@[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 : π•œ) :
@[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 : π•œ) :
@[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_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 : gcd_monoid.gcd m 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 : gcd_monoid.gcd m.nat_abs 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.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.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)] [floor_ring π•œ] {u : add_circle p} (h : is_of_fin_add_order u) :
@[protected, instance]

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]

The "additive circle" ℝ β§Έ (β„€ βˆ™ p) is normal.

@[protected, instance]

The "additive circle" ℝ β§Έ (β„€ βˆ™ p) is second-countable.

@[reducible]

The unit circle ℝ β§Έ β„€.