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.instMulActionNNRatToMonoidToMonoidWithZeroToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringInstNNRatLinearOrderedSemifield {α : Type u_1} [MulAction ℚ α] : MulAction ℚ≥0 α

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NNRat.coe_indicator {α : Type u_1} (s : Set α) (f : α → ℚ≥0) (a : α) : ↑(Set.indicator s f a) = Set.indicator s (fun (x : α) => ↑(f x)) a

theorem Rat.toNNRat_inv (q : ℚ) : Rat.toNNRat q⁻¹ = (Rat.toNNRat q)⁻¹

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

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

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 = Eq.mpr ⋯ (h q.num q.den)