Documentation

Mathlib.Topology.Instances.AddCircle.Real

The additive circle over #

Results specific to the additive circle over .

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
    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]
      theorem ZMod.toAddCircle_inj {N : } [NeZero N] {j k : ZMod N} :
      @[simp]
      theorem ZMod.toAddCircle_eq_zero {N : } [NeZero N] {j : ZMod N} :
      toAddCircle j = 0 j = 0