Documentation

Mathlib.Data.Dyadic

Dyadic rationals #

This file provides general API for Dyadic rationals that are used in Mathlib but not available in core.

source
@[instance_reducible]
instance instLinearOrderDyadic :
LinearOrder Dyadic
Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
instance instAddCommGroupDyadic :
AddCommGroup Dyadic
Equations
  • One or more equations did not get rendered due to their size.
source
def Dyadic.step (prec : ℤ) :
Dyadic

One unit on the dyadic grid with precision prec.

Equations
Instances For
    source
    theorem Dyadic.ofIntWithPrec_one (prec : ℤ) :
    ofIntWithPrec 1 prec = step prec
    source
    def Dyadic.toReal (d : Dyadic) :
    ℝ

    Interpret a dyadic rational as a real number.

    Equations
    Instances For
      source
      @[simp]
      theorem Dyadic.toReal_natCast (n : ℕ) :
      (↑n).toReal = ↑n
      source
      @[simp]
      theorem Dyadic.toReal_ofNat (n : ℕ) [n.AtLeastTwo] :
      (OfNat.ofNat n).toReal = OfNat.ofNat n
      source
      @[simp]
      theorem Dyadic.toReal_intCast (z : ℤ) :
      (↑z).toReal = ↑z
      source
      @[simp]
      theorem Dyadic.toReal_add (a b : Dyadic) :
      (a + b).toReal = a.toReal + b.toReal
      source
      @[simp]
      theorem Dyadic.toReal_mul (a b : Dyadic) :
      (a * b).toReal = a.toReal * b.toReal
      source
      @[simp]
      theorem Dyadic.toReal_pow (a : Dyadic) (n : ℕ) :
      (a ^ n).toReal = a.toReal ^ n
      source
      def Dyadic.toRealAddMonoidHom :
      Dyadic →+ ℝ

      Dyadic.toReal as an additive monoid homomorphism.

      Equations
      Instances For
        source
        @[simp]
        theorem Dyadic.toReal_le_toReal {a b : Dyadic} :
        a.toReal ≤ b.toReal ↔ a ≤ b
        source
        @[simp]
        theorem Dyadic.toReal_lt_toReal {a b : Dyadic} :
        a.toReal < b.toReal ↔ a < b
        source
        def Dyadic.toRealOrderEmbedding :
        Dyadic ↪o ℝ

        Dyadic.toReal as an order embedding.

        Equations
        Instances For