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.instDenselyOrdered : DenselyOrdered NNRat

Equations

• NNRat.instDenselyOrdered = ⋯

@[simp]

theorem NNRat.coe_inv (q : NNRat) : ↑q⁻¹ = (↑q)⁻¹

@[simp]

theorem NNRat.coe_div (p : NNRat) (q : NNRat) : ↑(p / q) = ↑p / ↑q

instance NNRat.instMulActionNNRatToMonoidToMonoidWithZeroToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifield {α : Type u_1} [MulAction ℚ α] : MulAction NNRat α

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

Equations

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

instance NNRat.instDistribMulActionNNRatToMonoidToMonoidWithZeroToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifieldToAddMonoid {α : Type u_1} [AddCommMonoid α] [DistribMulAction ℚ α] : DistribMulAction NNRat α

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 : α → NNRat) (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 : NNRat) : ↑q.num / ↑q.den = q

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

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

Equations

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