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.

instance NNRat.instMulActionOfRat {α : Type u_1} [MulAction ℚ α] : MulAction ℚ≥0 α

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

Equations

• NNRat.instMulActionOfRat = MulAction.compHom α ↑NNRat.coeHom

instance NNRat.instDistribMulActionOfRat {α : Type u_1} [AddCommMonoid α] [DistribMulAction ℚ α] : DistribMulAction ℚ≥0 α

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

Equations

• NNRat.instDistribMulActionOfRat = DistribMulAction.compHom α ↑NNRat.coeHom

@[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_inv (q : ℚ) : q⁻¹.toNNRat = q.toNNRat⁻¹

theorem Rat.toNNRat_div {p : ℚ} {q : ℚ} (hp : 0 ≤ p) : (p / q).toNNRat = p.toNNRat / q.toNNRat

theorem Rat.toNNRat_div' {p : ℚ} {q : ℚ} (hq : 0 ≤ q) : (p / q).toNNRat = p.toNNRat / q.toNNRat

Numerator and denominator

@[simp]

theorem NNRat.num_div_den (q : ℚ≥0) : ↑q.num / ↑q.den = q

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

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

Equations

• NNRat.rec h q = ⋯.mpr (h q.num q.den)