Documentation

Mathlib.Topology.Instances.AddCircle

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

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 #

theorem continuous_right_toIcoMod {๐•œ : Type u_1} [AddCommGroup ๐•œ] [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a x : ๐•œ) :
theorem continuous_left_toIocMod {๐•œ : Type u_1} [AddCommGroup ๐•œ] [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a x : ๐•œ) :
theorem toIcoMod_eventuallyEq_toIocMod {๐•œ : Type u_1} [AddCommGroup ๐•œ] [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
theorem continuousAt_toIcoMod {๐•œ : Type u_1} [AddCommGroup ๐•œ] [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
theorem continuousAt_toIocMod {๐•œ : Type u_1} [AddCommGroup ๐•œ] [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
@[reducible, inline]
abbrev AddCircle {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) :
Type u_1

The "additive circle": ๐•œ โงธ (โ„ค โˆ™ p). See also Circle and Real.angle.

Equations
    Instances For
      theorem AddCircle.coe_nsmul {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) {n : โ„•} {x : ๐•œ} :
      โ†‘(n โ€ข x) = n โ€ข โ†‘x
      theorem AddCircle.coe_zsmul {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) {n : โ„ค} {x : ๐•œ} :
      โ†‘(n โ€ข x) = n โ€ข โ†‘x
      theorem AddCircle.coe_add {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p x y : ๐•œ) :
      โ†‘(x + y) = โ†‘x + โ†‘y
      theorem AddCircle.coe_sub {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p x y : ๐•œ) :
      โ†‘(x - y) = โ†‘x - โ†‘y
      theorem AddCircle.coe_neg {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) {x : ๐•œ} :
      โ†‘(-x) = -โ†‘x
      theorem AddCircle.coe_zero {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) :
      โ†‘0 = 0
      theorem AddCircle.coe_eq_zero_iff {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) {x : ๐•œ} :
      โ†‘x = 0 โ†” โˆƒ (n : โ„ค), n โ€ข p = x
      theorem AddCircle.coe_period {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) :
      โ†‘p = 0
      theorem AddCircle.coe_add_period {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p x : ๐•œ) :
      โ†‘(x + p) = โ†‘x
      theorem AddCircle.continuous_mk' {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [TopologicalSpace ๐•œ] :
      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
      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
        Instances For
          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
            Instances For
              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
                Instances For
                  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
                    Instances For
                      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
                      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
                      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
                      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
                      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
                      theorem AddCircle.continuous_equivIco_symm {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] :
                      Continuous โ‡‘(equivIco p a).symm
                      theorem AddCircle.continuous_equivIoc_symm {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] :
                      Continuous โ‡‘(equivIoc p a).symm
                      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
                      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
                      def AddCircle.partialHomeomorphCoe {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] :

                      The quotient map ๐•œ โ†’ AddCircle p as a partial homeomorphism.

                      Equations
                        Instances For
                          @[simp]
                          theorem AddCircle.partialHomeomorphCoe_target {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] :
                          @[simp]
                          theorem AddCircle.partialHomeomorphCoe_symm_apply {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] (x : AddCircle p) :
                          โ†‘(partialHomeomorphCoe p a).symm x = โ†‘((equivIco p a) x)
                          @[simp]
                          theorem AddCircle.partialHomeomorphCoe_apply {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] (aโœ : ๐•œ) :
                          โ†‘(partialHomeomorphCoe p a) aโœ = โ†‘aโœ
                          @[simp]
                          theorem AddCircle.partialHomeomorphCoe_source {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] :
                          theorem AddCircle.isLocalHomeomorph_coe {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] [DenselyOrdered ๐•œ] :
                          @[simp]
                          theorem AddCircle.coe_image_Ico_eq {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] :

                          The image of the closed-open interval [a, a + p) under the quotient map ๐•œ โ†’ AddCircle p is the entire space.

                          @[simp]
                          theorem AddCircle.coe_image_Ioc_eq {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] :

                          The image of the closed-open interval [a, a + p) under the quotient map ๐•œ โ†’ AddCircle p is the entire space.

                          @[simp]
                          theorem AddCircle.coe_image_Icc_eq {๐•œ : Type u_1} [AddCommGroup ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] :

                          The image of the closed interval [0, p] under the quotient map ๐•œ โ†’ AddCircle p is the entire space.

                          def AddCircle.equivAddCircle {๐•œ : Type u_1} [Field ๐•œ] (p q : ๐•œ) (hp : p โ‰  0) (hq : q โ‰  0) :

                          The rescaling equivalence between additive circles with different periods.

                          Equations
                            Instances For
                              @[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))
                              @[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))
                              def AddCircle.homeomorphAddCircle {๐•œ : Type u_1} [Field ๐•œ] (p q : ๐•œ) [LinearOrder ๐•œ] [IsStrictOrderedRing ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] (hp : p โ‰  0) (hq : q โ‰  0) :

                              The rescaling homeomorphism between additive circles with different periods.

                              Equations
                                Instances For
                                  @[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))
                                  @[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))
                                  theorem AddCircle.natCast_div_mul_eq_nsmul {๐•œ : Type u_1} [Field ๐•œ] (p q r : ๐•œ) (m : โ„•) :
                                  โ†‘(โ†‘m / q * r) = m โ€ข โ†‘(r / q)
                                  theorem AddCircle.intCast_div_mul_eq_zsmul {๐•œ : Type u_1} [Field ๐•œ] (p q r : ๐•œ) (m : โ„ค) :
                                  โ†‘(โ†‘m / q * r) = m โ€ข โ†‘(r / q)
                                  @[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
                                  instance AddCircle.instDivisibleByInt {๐•œ : Type u_1} [Field ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsStrictOrderedRing ๐•œ] [hp : Fact (0 < p)] [FloorRing ๐•œ] :
                                  Equations
                                    theorem AddCircle.addOrderOf_period_div {๐•œ : Type u_1} [Field ๐•œ] {p : ๐•œ} [LinearOrder ๐•œ] [IsStrictOrderedRing ๐•œ] [hp : Fact (0 < p)] {n : โ„•} (h : 0 < n) :
                                    addOrderOf โ†‘(p / โ†‘n) = n
                                    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
                                    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
                                    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
                                    theorem AddCircle.addOrderOf_coe_rat {๐•œ : Type u_1} [Field ๐•œ] {p : ๐•œ} [LinearOrder ๐•œ] [IsStrictOrderedRing ๐•œ] [hp : Fact (0 < p)] {q : โ„š} :
                                    addOrderOf โ†‘(โ†‘q * p) = q.den
                                    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
                                    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
                                    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
                                    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
                                    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
                                      Instances For
                                        @[simp]
                                        theorem AddCircle.card_addOrderOf_eq_totient {๐•œ : Type u_1} [Field ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsStrictOrderedRing ๐•œ] [hp : Fact (0 < p)] {n : โ„•} :
                                        theorem AddCircle.finite_setOf_addOrderOf_eq {๐•œ : Type u_1} [Field ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsStrictOrderedRing ๐•œ] [hp : Fact (0 < p)] {n : โ„•} (hn : 0 < n) :
                                        @[deprecated AddCircle.finite_setOf_addOrderOf_eq (since := "2025-03-26")]
                                        theorem AddCircle.finite_setOf_add_order_eq {๐•œ : Type u_1} [Field ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsStrictOrderedRing ๐•œ] [hp : Fact (0 < p)] {n : โ„•} (hn : 0 < n) :

                                        Alias of AddCircle.finite_setOf_addOrderOf_eq.

                                        theorem AddCircle.finite_torsion {๐•œ : Type u_1} [Field ๐•œ] (p : ๐•œ) [LinearOrder ๐•œ] [IsStrictOrderedRing ๐•œ] [hp : Fact (0 < p)] {n : โ„•} (hn : 0 < n) :

                                        The "additive circle" โ„ โงธ (โ„ค โˆ™ p) is compact.

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

                                        @[reducible, inline]

                                        The unit circle โ„ โงธ โ„ค.

                                        Equations
                                          Instances For

                                            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.

                                            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).

                                            Instances For
                                              def AddCircle.equivIccQuot {๐•œ : Type u_1} [AddCommGroup ๐•œ] [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] (p a : ๐•œ) [hp : Fact (0 < p)] [Archimedean ๐•œ] :

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

                                              Equations
                                                Instances For
                                                  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, โ‹ฏโŸฉ
                                                  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, โ‹ฏโŸฉ
                                                  def AddCircle.homeoIccQuot {๐•œ : Type u_1} [AddCommGroup ๐•œ] [LinearOrder ๐•œ] [IsOrderedAddMonoid ๐•œ] (p a : ๐•œ) [hp : Fact (0 < p)] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] :

                                                  The natural map from [a, a + p] โŠ‚ ๐•œ with endpoints identified to ๐•œ / โ„ค โ€ข p, as a homeomorphism of topological spaces.

                                                  Equations
                                                    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.

                                                      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)
                                                      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
                                                      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))) :
                                                      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)) :
                                                      @[simp]
                                                      theorem AddCircle.coe_fract (x : โ„) :
                                                      โ†‘(Int.fract x) = โ†‘x
                                                      noncomputable def ZMod.toAddCircle {N : โ„•} [NeZero N] :

                                                      The AddMonoidHom from ZMod N to โ„ / โ„ค sending j mod N to j / N mod 1.

                                                      Equations
                                                        Instances For
                                                          theorem ZMod.toAddCircle_intCast {N : โ„•} [NeZero N] (j : โ„ค) :
                                                          toAddCircle โ†‘j = โ†‘(โ†‘j / โ†‘N)
                                                          theorem ZMod.toAddCircle_natCast {N : โ„•} [NeZero N] (j : โ„•) :
                                                          toAddCircle โ†‘j = โ†‘(โ†‘j / โ†‘N)
                                                          theorem ZMod.toAddCircle_apply {N : โ„•} [NeZero N] (j : ZMod N) :
                                                          toAddCircle j = โ†‘(โ†‘j.val / โ†‘N)

                                                          Explicit formula for toCircle j. Note that this is "evil" because it uses ZMod.val. Where possible, it is recommended to lift j to โ„ค and use toAddCircle_intCast instead.

                                                          @[simp]
                                                          @[simp]
                                                          theorem ZMod.toAddCircle_eq_zero {N : โ„•} [NeZero N] {j : ZMod N} :