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} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) (x : ๐•œ) :
theorem continuous_left_toIocMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) (x : ๐•œ) :
theorem toIcoMod_eventuallyEq_toIocMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
theorem continuousAt_toIcoMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
theorem continuousAt_toIocMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {p : ๐•œ} (hp : 0 < p) (a : ๐•œ) {x : ๐•œ} (hx : โ†‘x โ‰  โ†‘a) :
@[reducible, inline]
abbrev AddCircle {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) :
Type u_1

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

Equations
Instances For
    theorem AddCircle.coe_nsmul {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) {n : โ„•} {x : ๐•œ} :
    โ†‘(n โ€ข x) = n โ€ข โ†‘x
    theorem AddCircle.coe_zsmul {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) {n : โ„ค} {x : ๐•œ} :
    โ†‘(n โ€ข x) = n โ€ข โ†‘x
    theorem AddCircle.coe_add {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) (x : ๐•œ) (y : ๐•œ) :
    โ†‘(x + y) = โ†‘x + โ†‘y
    theorem AddCircle.coe_sub {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) (x : ๐•œ) (y : ๐•œ) :
    โ†‘(x - y) = โ†‘x - โ†‘y
    theorem AddCircle.coe_neg {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) {x : ๐•œ} :
    โ†‘(-x) = -โ†‘x
    theorem AddCircle.coe_eq_zero_iff {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) {x : ๐•œ} :
    โ†‘x = 0 โ†” โˆƒ (n : โ„ค), n โ€ข p = x
    theorem AddCircle.coe_eq_zero_of_pos_iff {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) (hp : 0 < p) {x : ๐•œ} (hx : 0 < x) :
    โ†‘x = 0 โ†” โˆƒ (n : โ„•), n โ€ข p = x
    theorem AddCircle.coe_period {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) :
    โ†‘p = 0
    theorem AddCircle.coe_add_period {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) (x : ๐•œ) :
    โ†‘(x + p) = โ†‘x
    theorem AddCircle.continuous_mk' {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [TopologicalSpace ๐•œ] :
    def AddCircle.equivIco {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [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} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [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} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [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} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [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} [LinearOrderedAddCommGroup ๐•œ] {p : ๐•œ} [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} [LinearOrderedAddCommGroup ๐•œ] {p : ๐•œ} [hp : Fact (0 < p)] {a : ๐•œ} [Archimedean ๐•œ] {f : ๐•œ โ†’ B} {x : ๐•œ} (hx : x โˆˆ Set.Ico a (a + p)) :
            AddCircle.liftIco p a f โ†‘x = f x
            theorem AddCircle.liftIoc_coe_apply {๐•œ : Type u_1} {B : Type u_2} [LinearOrderedAddCommGroup ๐•œ] {p : ๐•œ} [hp : Fact (0 < p)] {a : ๐•œ} [Archimedean ๐•œ] {f : ๐•œ โ†’ B} {x : ๐•œ} (hx : x โˆˆ Set.Ioc a (a + p)) :
            AddCircle.liftIoc p a f โ†‘x = f x
            theorem AddCircle.eq_coe_Ico {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] {p : ๐•œ} [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} [LinearOrderedAddCommGroup ๐•œ] {p : ๐•œ} [hp : Fact (0 < p)] {a : ๐•œ} [Archimedean ๐•œ] (ha : a โˆˆ Set.Ico 0 p) :
            โ†‘a = 0 โ†” a = 0
            theorem AddCircle.continuous_equivIco_symm {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] :
            Continuous โ‡‘(AddCircle.equivIco p a).symm
            theorem AddCircle.continuous_equivIoc_symm {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] :
            Continuous โ‡‘(AddCircle.equivIoc p a).symm
            theorem AddCircle.continuousAt_equivIco {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {x : AddCircle p} (hx : x โ‰  โ†‘a) :
            theorem AddCircle.continuousAt_equivIoc {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] {x : AddCircle p} (hx : x โ‰  โ†‘a) :
            @[simp]
            theorem AddCircle.partialHomeomorphCoe_symm_apply {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] (x : AddCircle p) :
            โ†‘(AddCircle.partialHomeomorphCoe p a).symm x = โ†‘((AddCircle.equivIco p a) x)
            @[simp]
            theorem AddCircle.partialHomeomorphCoe_apply {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] (a : ๐•œ) :
            โ†‘(AddCircle.partialHomeomorphCoe p aโœ) a = โ†‘a
            @[simp]
            theorem AddCircle.partialHomeomorphCoe_source {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] :
            @[simp]
            theorem AddCircle.partialHomeomorphCoe_target {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] :
            def AddCircle.partialHomeomorphCoe {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] (a : ๐•œ) [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] :

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

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem AddCircle.isLocalHomeomorph_coe {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [DiscreteTopology โ†ฅ(AddSubgroup.zmultiples p)] [DenselyOrdered ๐•œ] :
              IsLocalHomeomorph QuotientAddGroup.mk
              @[simp]
              theorem AddCircle.coe_image_Ico_eq {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [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.

              @[simp]
              theorem AddCircle.coe_image_Ioc_eq {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [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.

              @[simp]
              theorem AddCircle.coe_image_Icc_eq {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) [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.

              def AddCircle.equivAddCircle {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (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} [LinearOrderedField ๐•œ] (p : ๐•œ) (q : ๐•œ) (hp : p โ‰  0) (hq : q โ‰  0) (x : ๐•œ) :
                (AddCircle.equivAddCircle p q hp hq) โ†‘x = โ†‘(x * (pโปยน * q))
                @[simp]
                theorem AddCircle.equivAddCircle_symm_apply_mk {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (p : ๐•œ) (q : ๐•œ) (hp : p โ‰  0) (hq : q โ‰  0) (x : ๐•œ) :
                (AddCircle.equivAddCircle p q hp hq).symm โ†‘x = โ†‘(x * (qโปยน * p))
                def AddCircle.homeomorphAddCircle {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (p : ๐•œ) (q : ๐•œ) [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} [LinearOrderedField ๐•œ] (p : ๐•œ) (q : ๐•œ) [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] (hp : p โ‰  0) (hq : q โ‰  0) (x : ๐•œ) :
                  (AddCircle.homeomorphAddCircle p q hp hq) โ†‘x = โ†‘(x * (pโปยน * q))
                  @[simp]
                  theorem AddCircle.homeomorphAddCircle_symm_apply_mk {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (p : ๐•œ) (q : ๐•œ) [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] (hp : p โ‰  0) (hq : q โ‰  0) (x : ๐•œ) :
                  (AddCircle.homeomorphAddCircle p q hp hq).symm โ†‘x = โ†‘(x * (qโปยน * p))
                  @[simp]
                  theorem AddCircle.coe_equivIco_mk_apply {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] [FloorRing ๐•œ] (x : ๐•œ) :
                  โ†‘((AddCircle.equivIco p 0) โ†‘x) = Int.fract (x / p) * p
                  instance AddCircle.instDivisibleByInt {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] [FloorRing ๐•œ] :
                  Equations
                  theorem AddCircle.addOrderOf_period_div {๐•œ : Type u_1} [LinearOrderedField ๐•œ] {p : ๐•œ} [hp : Fact (0 < p)] {n : โ„•} (h : 0 < n) :
                  addOrderOf โ†‘(p / โ†‘n) = n
                  theorem AddCircle.gcd_mul_addOrderOf_div_eq {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (p : ๐•œ) [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} [LinearOrderedField ๐•œ] {p : ๐•œ} [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} [LinearOrderedField ๐•œ] {p : ๐•œ} [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} [LinearOrderedField ๐•œ] {p : ๐•œ} [hp : Fact (0 < p)] {q : โ„š} :
                  addOrderOf โ†‘(โ†‘q * p) = q.den
                  theorem AddCircle.addOrderOf_eq_pos_iff {๐•œ : Type u_1} [LinearOrderedField ๐•œ] {p : ๐•œ} [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} [LinearOrderedField ๐•œ] {p : ๐•œ} [hp : Fact (0 < p)] {u : AddCircle p} (h : IsOfFinAddOrder u) :
                  โˆƒ (m : โ„•), m.gcd (addOrderOf u) = 1 โˆง m < addOrderOf u โˆง โ†‘(โ†‘m / โ†‘(addOrderOf u) * p) = u
                  def AddCircle.setAddOrderOfEquiv {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (p : ๐•œ) [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} [LinearOrderedField ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] {n : โ„•} :
                    Nat.card { u : AddCircle p // addOrderOf u = n } = n.totient
                    theorem AddCircle.finite_setOf_add_order_eq {๐•œ : Type u_1} [LinearOrderedField ๐•œ] (p : ๐•œ) [hp : Fact (0 < p)] {n : โ„•} (hn : 0 < n) :
                    {u : AddCircle p | addOrderOf u = n}.Finite
                    Equations
                    • โ‹ฏ = โ‹ฏ

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

                    Equations
                    • โ‹ฏ = โ‹ฏ

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

                    Equations
                    • โ‹ฏ = โ‹ฏ
                    instance instZeroLTOne {๐•œ : Type u_1} [StrictOrderedSemiring ๐•œ] :
                    Fact (0 < 1)
                    Equations
                    • โ‹ฏ = โ‹ฏ
                    @[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} [LinearOrderedAddCommGroup ๐•œ] (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} [LinearOrderedAddCommGroup ๐•œ] (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
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem AddCircle.equivIccQuot_comp_mk_eq_toIcoMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) (a : ๐•œ) [hp : Fact (0 < p)] [Archimedean ๐•œ] :
                          โ‡‘(AddCircle.equivIccQuot p a) โˆ˜ Quotient.mk'' = fun (x : ๐•œ) => Quot.mk (AddCircle.EndpointIdent p a) โŸจtoIcoMod โ‹ฏ a x, โ‹ฏโŸฉ
                          theorem AddCircle.equivIccQuot_comp_mk_eq_toIocMod {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (p : ๐•œ) (a : ๐•œ) [hp : Fact (0 < p)] [Archimedean ๐•œ] :
                          โ‡‘(AddCircle.equivIccQuot p a) โˆ˜ Quotient.mk'' = fun (x : ๐•œ) => Quot.mk (AddCircle.EndpointIdent p a) โŸจtoIocMod โ‹ฏ a x, โ‹ฏโŸฉ
                          def AddCircle.homeoIccQuot {๐•œ : Type u_1} [LinearOrderedAddCommGroup ๐•œ] (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} [LinearOrderedAddCommGroup ๐•œ] {p : ๐•œ} {a : ๐•œ} [hp : Fact (0 < p)] [Archimedean ๐•œ] {f : ๐•œ โ†’ B} (h : f a = f (a + p)) :
                            AddCircle.liftIco p a f = Quot.lift ((Set.Icc a (a + p)).restrict f) โ‹ฏ โˆ˜ โ‡‘(AddCircle.equivIccQuot p a)
                            theorem AddCircle.liftIco_zero_coe_apply {๐•œ : Type u_1} {B : Type u_2} [LinearOrderedAddCommGroup ๐•œ] {p : ๐•œ} [hp : Fact (0 < p)] [Archimedean ๐•œ] {f : ๐•œ โ†’ B} {x : ๐•œ} (hx : x โˆˆ Set.Ico 0 p) :
                            AddCircle.liftIco p 0 f โ†‘x = f x
                            theorem AddCircle.liftIco_continuous {๐•œ : Type u_1} {B : Type u_2} [LinearOrderedAddCommGroup ๐•œ] {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} [LinearOrderedAddCommGroup ๐•œ] {p : ๐•œ} [hp : Fact (0 < p)] [Archimedean ๐•œ] [TopologicalSpace ๐•œ] [OrderTopology ๐•œ] [TopologicalSpace B] {f : ๐•œ โ†’ B} (hf : f 0 = f p) (hc : ContinuousOn f (Set.Icc 0 p)) :
                            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 : โ„ค) :
                              ZMod.toAddCircle โ†‘j = โ†‘(โ†‘j / โ†‘N)
                              theorem ZMod.toAddCircle_natCast {N : โ„•} [NeZero N] (j : โ„•) :
                              ZMod.toAddCircle โ†‘j = โ†‘(โ†‘j / โ†‘N)
                              theorem ZMod.toAddCircle_apply {N : โ„•} [NeZero N] (j : ZMod N) :
                              ZMod.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.

                              theorem ZMod.toAddCircle_injective (N : โ„•) [NeZero N] :
                              Function.Injective โ‡‘ZMod.toAddCircle
                              @[simp]
                              theorem ZMod.toAddCircle_inj {N : โ„•} [NeZero N] {j : ZMod N} {k : ZMod N} :
                              ZMod.toAddCircle j = ZMod.toAddCircle k โ†” j = k
                              @[simp]
                              theorem ZMod.toAddCircle_eq_zero {N : โ„•} [NeZero N] {j : ZMod N} :
                              ZMod.toAddCircle j = 0 โ†” j = 0