# The additive circle #

We define the additive circle `AddCircle p` as the quotient `𝕜 ⧸ (ℤ ∙ p)` for some period `p : 𝕜`.

See also `Circle` and `Real.angle`. For the normed group structure on `AddCircle`, see `AddCircle.NormedAddCommGroup` in a later file.

## Main definitions and results: #

- `AddCircle`: the additive circle `𝕜 ⧸ (ℤ ∙ p)` for some period `p : 𝕜`
- `UnitAddCircle`: the special case `ℝ ⧸ ℤ`
- `AddCircle.equivAddCircle`: the rescaling equivalence `AddCircle p ≃+ AddCircle q`
- `AddCircle.equivIco` and `AddCircle.equivIoc`: the natural equivalences `AddCircle p ≃ Ico a (a + p)` and `AddCircle p ≃ Ioc a (a + p)`
- `AddCircle.addOrderOf_div_of_gcd_eq_one`: rational points have finite order
- `AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder`: finite-order points are rational
- `AddCircle.homeoIccQuot`: the natural topological equivalence between `AddCircle p` and `Icc a (a + p)` with its endpoints identified.
- `AddCircle.liftIco_continuous` and `AddCircle.liftIoc_continuous`: if `f : ℝ → B` is continuous, and `f a = f (a + p)` for some `a`, then there is a continuous function `AddCircle 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 `AddCircle (1 : ℚ)`, and so we set things up more generally.

## TODO #

- Link with periodicity
- Lie group structure
- Exponential equivalence to `Circle`

source
theorem continuous_right_toIcoMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) :
ContinuousWithinAt (toIcoMod hp a) (Set.Ici x) x
source
theorem continuous_left_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a x : 𝕜) :
ContinuousWithinAt (toIocMod hp a) (Set.Iic x) x
source
theorem toIcoMod_eventuallyEq_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ↑x ≠ ↑a) :
toIcoMod hp a =ᶠ[nhds x] toIocMod hp a
source
theorem continuousAt_toIcoMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ↑x ≠ ↑a) :
ContinuousAt (toIcoMod hp a) x
source
theorem continuousAt_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜} (hx : ↑x ≠ ↑a) :
ContinuousAt (toIocMod hp a) x
source
@[reducible, inline]
abbrev AddCircle {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) :
Type u_1

The "additive circle": `𝕜 ⧸ (ℤ ∙ p)`. See also `Circle` and `Real.angle`.

Equations

- AddCircle p = (𝕜 ⧸ AddSubgroup.zmultiples p)

Instances For

source
theorem AddCircle.coe_nsmul {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {n : ℕ} {x : 𝕜} :
↑(n • x) = n • ↑x
source
theorem AddCircle.coe_zsmul {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {n : ℤ} {x : 𝕜} :
↑(n • x) = n • ↑x
source
theorem AddCircle.coe_add {𝕜 : Type u_1} [AddCommGroup 𝕜] (p x y : 𝕜) :
↑(x + y) = ↑x + ↑y
source
theorem AddCircle.coe_sub {𝕜 : Type u_1} [AddCommGroup 𝕜] (p x y : 𝕜) :
↑(x - y) = ↑x - ↑y
source
theorem AddCircle.coe_neg {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {x : 𝕜} :
↑(-x) = -↑x
source
theorem AddCircle.coe_zero {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) :
↑0 = 0
source
theorem AddCircle.coe_eq_zero_iff {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) {x : 𝕜} :
↑x = 0 ↔ ∃ (n : ℤ), n • p = x
source
theorem AddCircle.coe_period {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) :
↑p = 0
source
theorem AddCircle.coe_add_period {𝕜 : Type u_1} [AddCommGroup 𝕜] (p x : 𝕜) :
↑(x + p) = ↑x
source
theorem AddCircle.continuous_mk' {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [TopologicalSpace 𝕜] :
Continuous ⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p))
source
theorem AddCircle.coe_eq_zero_of_pos_iff {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (hp : 0 < p) {x : 𝕜} (hx : 0 < x) :
↑x = 0 ↔ ∃ (n : ℕ), n • p = x
source
def AddCircle.equivIco {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] :
AddCircle p ≃ ↑(Set.Ico a (a + p))

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

Equations

- AddCircle.equivIco p a = QuotientAddGroup.equivIcoMod ⋯ a

Instances For

source
def AddCircle.equivIoc {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] :
AddCircle p ≃ ↑(Set.Ioc a (a + p))

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

Equations

- AddCircle.equivIoc p a = QuotientAddGroup.equivIocMod ⋯ a

Instances For

source
def AddCircle.liftIco {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] (f : 𝕜 → B) :
AddCircle p → B

Given a function on `𝕜`, return the unique function on `AddCircle p` agreeing with `f` on `[a, a + p)`.

Equations

- AddCircle.liftIco p a f = (Set.Ico a (a + p)).restrict f ∘ ⇑(AddCircle.equivIco p a)

Instances For

source
def AddCircle.liftIoc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] (f : 𝕜 → B) :
AddCircle p → B

Given a function on `𝕜`, return the unique function on `AddCircle p` agreeing with `f` on `(a, a + p]`.

Equations

- AddCircle.liftIoc p a f = (Set.Ioc a (a + p)).restrict f ∘ ⇑(AddCircle.equivIoc p a)

Instances For

source
theorem AddCircle.equivIco_coe_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {x : 𝕜} (hx : x ∈ Set.Ico a (a + p)) :
(equivIco p a) ↑x = ⟨x, hx⟩
source
theorem AddCircle.equivIoc_coe_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {x : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) :
(equivIoc p a) ↑x = ⟨x, hx⟩
source
theorem AddCircle.coe_eq_coe_iff_of_mem_Ico {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {x y : 𝕜} (hx : x ∈ Set.Ico a (a + p)) (hy : y ∈ Set.Ico a (a + p)) :
↑x = ↑y ↔ x = y
source
theorem AddCircle.liftIco_coe_apply {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Set.Ico a (a + p)) :
liftIco p a f ↑x = f x
source
theorem AddCircle.liftIoc_coe_apply {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Set.Ioc a (a + p)) :
liftIoc p a f ↑x = f x
source
theorem AddCircle.liftIco_comp_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {β : Type u_4} {f : 𝕜 → α} {g : α → β} {a : 𝕜} {x : AddCircle p} :
liftIco p a (g ∘ f) x = g (liftIco p a f x)
source
theorem AddCircle.liftIoc_comp_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {β : Type u_4} {f : 𝕜 → α} {g : α → β} {a : 𝕜} {x : AddCircle p} :
liftIoc p a (g ∘ f) x = g (liftIoc p a f x)
source
theorem AddCircle.eq_coe_Ico {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] (a : AddCircle p) :
∃ b ∈ Set.Ico 0 p, ↑b = a
source
theorem AddCircle.coe_eq_zero_iff_of_mem_Ico {𝕜 : Type u_1} [AddCommGroup 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] {a : 𝕜} [Archimedean 𝕜] (ha : a ∈ Set.Ico 0 p) :
↑a = 0 ↔ a = 0
source
theorem AddCircle.continuous_equivIco_symm {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] :
Continuous ⇑(equivIco p a).symm
source
theorem AddCircle.continuous_equivIoc_symm {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] :
Continuous ⇑(equivIoc p a).symm
source
theorem AddCircle.continuousAt_equivIco {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {x : AddCircle p} (hx : x ≠ ↑a) :
ContinuousAt (⇑(equivIco p a)) x
source
theorem AddCircle.continuousAt_equivIoc {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {x : AddCircle p} (hx : x ≠ ↑a) :
ContinuousAt (⇑(equivIoc p a)) x
source
def AddCircle.openPartialHomeomorphCoe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] :
OpenPartialHomeomorph 𝕜 (AddCircle p)

The quotient map `𝕜 → AddCircle p` as an open partial homeomorphism.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem AddCircle.openPartialHomeomorphCoe_source {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] :
(openPartialHomeomorphCoe p a).source = Set.Ioo a (a + p)
source
@[simp]
theorem AddCircle.openPartialHomeomorphCoe_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] (a✝ : 𝕜) :
↑(openPartialHomeomorphCoe p a) a✝ = ↑a✝
source
@[simp]
theorem AddCircle.openPartialHomeomorphCoe_symm_apply {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] (x : AddCircle p) :
↑(openPartialHomeomorphCoe p a).symm x = ↑((equivIco p a) x)
source
@[simp]
theorem AddCircle.openPartialHomeomorphCoe_target {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] :
(openPartialHomeomorphCoe p a).target = {↑a}ᶜ
source
@[deprecated AddCircle.openPartialHomeomorphCoe (since := "2025-08-29")]
def AddCircle.partialHomeomorphCoe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] :
OpenPartialHomeomorph 𝕜 (AddCircle p)

Alias of `AddCircle.openPartialHomeomorphCoe`.

The quotient map `𝕜 → AddCircle p` as an open partial homeomorphism.

Equations

- @AddCircle.partialHomeomorphCoe = @AddCircle.openPartialHomeomorphCoe

Instances For

source
theorem AddCircle.isLocalHomeomorph_coe {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [DiscreteTopology ↥(AddSubgroup.zmultiples p)] [DenselyOrdered 𝕜] :
IsLocalHomeomorph QuotientAddGroup.mk
source
@[simp]
theorem AddCircle.coe_image_Ico_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] :
QuotientAddGroup.mk '' Set.Ico a (a + p) = Set.univ

The image of the closed-open interval `[a, a + p)` under the quotient map `𝕜 → AddCircle p` is the entire space.

source
@[simp]
theorem AddCircle.coe_image_Ioc_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] :
QuotientAddGroup.mk '' Set.Ioc a (a + p) = Set.univ

The image of the closed-open interval `[a, a + p)` under the quotient map `𝕜 → AddCircle p` is the entire space.

source
@[simp]
theorem AddCircle.coe_image_Icc_eq {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] (a : 𝕜) [Archimedean 𝕜] :
QuotientAddGroup.mk '' Set.Icc a (a + p) = Set.univ

The image of the closed interval `[0, p]` under the quotient map `𝕜 → AddCircle p` is the entire space.

source
theorem AddCircle.Ico_ext {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {f g : AddCircle p → α} (a : 𝕜) (h : ∀ x ∈ Set.Ico a (a + p), f ↑x = g ↑x) :
f = g

If functions on AddCircle agree on the image of the interval `[a, a + p)` then they are equal

source
theorem AddCircle.Ioc_ext {𝕜 : Type u_1} [AddCommGroup 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)] [Archimedean 𝕜] {α : Type u_3} {f g : AddCircle p → α} (a : 𝕜) (h : ∀ x ∈ Set.Ioc a (a + p), f ↑x = g ↑x) :
f = g

If functions on AddCircle agree on the image of the interval `(a, a + p]` then they are equal

source
def AddCircle.equivAddCircle {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) :
AddCircle p ≃+ AddCircle q

The rescaling equivalence between additive circles with different periods.

Equations

- AddCircle.equivAddCircle p q hp hq = QuotientAddGroup.congr (AddSubgroup.zmultiples p) (AddSubgroup.zmultiples q) (AddAut.mulRight ((Units.mk0 p hp)⁻¹ * Units.mk0 q hq)) ⋯

Instances For

source
@[simp]
theorem AddCircle.equivAddCircle_apply_mk {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
(equivAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))
source
@[simp]
theorem AddCircle.equivAddCircle_symm_apply_mk {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
(equivAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))
source
def AddCircle.homeomorphAddCircle {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) :
AddCircle p ≃ₜ AddCircle q

The rescaling homeomorphism between additive circles with different periods.

Equations

- AddCircle.homeomorphAddCircle p q hp hq = { toEquiv := ↑(AddCircle.equivAddCircle p q hp hq), continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source
@[simp]
theorem AddCircle.homeomorphAddCircle_apply_mk {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
(homeomorphAddCircle p q hp hq) ↑x = ↑(x * (p⁻¹ * q))
source
@[simp]
theorem AddCircle.homeomorphAddCircle_symm_apply_mk {𝕜 : Type u_1} [Field 𝕜] (p q : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] (hp : p ≠ 0) (hq : q ≠ 0) (x : 𝕜) :
(homeomorphAddCircle p q hp hq).symm ↑x = ↑(x * (q⁻¹ * p))
source
theorem AddCircle.natCast_div_mul_eq_nsmul {𝕜 : Type u_1} [Field 𝕜] (p q r : 𝕜) (m : ℕ) :
↑(↑m / q * r) = m • ↑(r / q)
source
theorem AddCircle.intCast_div_mul_eq_zsmul {𝕜 : Type u_1} [Field 𝕜] (p q r : 𝕜) (m : ℤ) :
↑(↑m / q * r) = m • ↑(r / q)
source
@[simp]
theorem AddCircle.coe_equivIco_mk_apply {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] [FloorRing 𝕜] (x : 𝕜) :
↑((equivIco p 0) ↑x) = Int.fract (x / p) * p
source
instance AddCircle.instDivisibleByInt {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] [FloorRing 𝕜] :
DivisibleBy (AddCircle p) ℤ
Equations

- AddCircle.instDivisibleByInt p = { div := fun (x : AddCircle p) (n : ℤ) => ↑((↑n)⁻¹ * ↑((AddCircle.equivIco p 0) x)), div_zero := ⋯, div_cancel := ⋯ }

source
@[simp]
theorem AddCircle.coe_fract {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [FloorRing 𝕜] (x : 𝕜) :
↑(Int.fract x) = ↑x
source
theorem AddCircle.addOrderOf_period_div {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (h : 0 < n) :
addOrderOf ↑(p / ↑n) = n
source
theorem AddCircle.gcd_mul_addOrderOf_div_eq {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (m : ℕ) (hn : 0 < n) :
m.gcd n * addOrderOf ↑(↑m / ↑n * p) = n
source
theorem AddCircle.addOrderOf_div_of_gcd_eq_one {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {m n : ℕ} (hn : 0 < n) (h : m.gcd n = 1) :
addOrderOf ↑(↑m / ↑n * p) = n
source
theorem AddCircle.addOrderOf_div_of_gcd_eq_one' {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {m : ℤ} {n : ℕ} (hn : 0 < n) (h : m.natAbs.gcd n = 1) :
addOrderOf ↑(↑m / ↑n * p) = n
source
theorem AddCircle.addOrderOf_coe_rat {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {q : ℚ} :
addOrderOf ↑(↑q * p) = q.den
source
theorem AddCircle.nsmul_eq_zero_iff {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} {n : ℕ} (h : 0 < n) :
n • u = 0 ↔ ∃ m < n, ↑(↑m / ↑n * p) = u
source
theorem AddCircle.addOrderOf_eq_pos_iff {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} {n : ℕ} (h : 0 < n) :
addOrderOf u = n ↔ ∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n * p) = u
source
theorem AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {u : AddCircle p} (h : IsOfFinAddOrder u) :
∃ (m : ℕ), m.gcd (addOrderOf u) = 1 ∧ m < addOrderOf u ∧ ↑(↑m / ↑(addOrderOf u) * p) = u
source
theorem AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {a : 𝕜} :
¬IsOfFinAddOrder ↑a ↔ ∀ (q : ℚ), ↑q ≠ a / p
source
theorem AddCircle.isOfFinAddOrder_iff_exists_rat_eq_div {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {a : 𝕜} :
IsOfFinAddOrder ↑a ↔ ∃ (q : ℚ), ↑q = a / p
source
@[deprecated AddCircle.not_isOfFinAddOrder_iff_forall_rat_ne_div (since := "2025-08-13")]
theorem AddCircle.addOrderOf_coe_eq_zero_iff_forall_rat_ne_div {𝕜 : Type u_1} [Field 𝕜] {p : 𝕜} [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {a : 𝕜} :
addOrderOf ↑a = 0 ↔ ∀ (q : ℚ), ↑q ≠ a / p
source
def AddCircle.setAddOrderOfEquiv {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (hn : 0 < n) :
↑{u : AddCircle p | addOrderOf 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 : AddCircle p)` where `m` is coprime to `n` and satisfies `0 ≤ m < n`.

Equations

- AddCircle.setAddOrderOfEquiv p hn = (Equiv.ofBijective (fun (m : ↑{m : ℕ | m < n ∧ m.gcd n = 1}) => ⟨↑(↑↑m / ↑n * p), ⋯⟩) ⋯).symm

Instances For

source
@[simp]
theorem AddCircle.card_addOrderOf_eq_totient {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} :
Nat.card { u : AddCircle p // addOrderOf u = n } = n.totient
source
theorem AddCircle.finite_setOf_addOrderOf_eq {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (hn : 0 < n) :
{u : AddCircle p | addOrderOf u = n}.Finite
source
theorem AddCircle.finite_torsion {𝕜 : Type u_1} [Field 𝕜] (p : 𝕜) [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {n : ℕ} (hn : 0 < n) :
{u : AddCircle p | n • u = 0}.Finite

This section proves that for any `a`, the natural map from `[a, a + p] ⊂ 𝕜` to `AddCircle p` gives an identification of `AddCircle p`, as a topological space, with the quotient of `[a, a + p]` by the equivalence relation identifying the endpoints.

source
inductive AddCircle.EndpointIdent {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (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)`.

- mk {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] : EndpointIdent p a ⟨a, ⋯⟩ ⟨a + p, ⋯⟩

Instances For

source
def AddCircle.equivIccQuot {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] :
AddCircle p ≃ Quot (EndpointIdent p a)

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem AddCircle.equivIccQuot_comp_mk_eq_toIcoMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] :
⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun (x : 𝕜) => Quot.mk (EndpointIdent p a) ⟨toIcoMod ⋯ a x, ⋯⟩
source
theorem AddCircle.equivIccQuot_comp_mk_eq_toIocMod {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] :
⇑(equivIccQuot p a) ∘ Quotient.mk'' = fun (x : 𝕜) => Quot.mk (EndpointIdent p a) ⟨toIocMod ⋯ a x, ⋯⟩
source
def AddCircle.homeoIccQuot {𝕜 : Type u_1} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] (p a : 𝕜) [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] :
AddCircle p ≃ₜ Quot (EndpointIdent p a)

The natural map from `[a, a + p] ⊂ 𝕜` with endpoints identified to `𝕜 / ℤ • p`, as a homeomorphism of topological spaces.

Equations

- AddCircle.homeoIccQuot p a = { toEquiv := AddCircle.equivIccQuot p a, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

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 `AddCircle p`, by first showing that various lifts are equivalent.

source
theorem AddCircle.liftIoc_eq_liftIco {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (hf : f a = f (a + p)) :
liftIoc p a f = liftIco p a f
source
theorem AddCircle.liftIco_eq_lift_Icc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)) :
liftIco p a f = Quot.lift ((Set.Icc a (a + p)).restrict f) ⋯ ∘ ⇑(equivIccQuot p a)
source
theorem AddCircle.liftIoc_eq_lift_Icc {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} (h : f a = f (a + p)) :
liftIoc p a f = Quot.lift ((Set.Icc a (a + p)).restrict f) ⋯ ∘ ⇑(equivIccQuot p a)
source
theorem AddCircle.liftIco_zero_coe_apply {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Set.Ico 0 p) :
liftIco p 0 f ↑x = f x
source
theorem AddCircle.liftIoc_zero_coe_apply {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜} (hx : x ∈ Set.Ioc 0 p) :
liftIoc p 0 f ↑x = f x
source
theorem AddCircle.liftIco_continuous {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p)) (hc : ContinuousOn f (Set.Icc a (a + p))) :
Continuous (liftIco p a f)
source
theorem AddCircle.liftIco_zero_continuous {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) :
Continuous (liftIco p 0 f)
source
theorem AddCircle.liftIoc_continuous {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p a : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f a = f (a + p)) (hc : ContinuousOn f (Set.Icc a (a + p))) :
Continuous (liftIoc p a f)
source
theorem AddCircle.liftIoc_zero_continuous {𝕜 : Type u_1} {B : Type u_2} [AddCommGroup 𝕜] [LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] {p : 𝕜} [hp : Fact (0 < p)] [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace B] {f : 𝕜 → B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) :
Continuous (liftIoc p 0 f)