Documentation

Mathlib.Data.NNRat.Lemmas

Field and action structures on the nonnegative rationals #

This file provides additional results about NNRat that cannot live in earlier files due to import cycles.

A MulAction over restricts to a MulAction over ℚ≥0.

Equations

    A DistribMulAction over restricts to a DistribMulAction over ℚ≥0.

    Equations
      @[simp]
      theorem NNRat.coe_indicator {α : Type u_1} (s : Set α) (f : αℚ≥0) (a : α) :
      (s.indicator f a) = s.indicator (fun (x : α) => (f x)) a
      theorem Rat.toNNRat_div {p q : } (hp : 0 p) :
      theorem Rat.toNNRat_div' {p q : } (hq : 0 q) :

      Numerator and denominator #

      def NNRat.rec {α : ℚ≥0Sort u_1} (h : (m n : ) → α (m / n)) (q : ℚ≥0) :
      α q

      A recursor for nonnegative rationals in terms of numerators and denominators.

      Equations
        Instances For