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

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)

theorem NNRat.mul_num (q₁ q₂ : ℚ≥0) : (q₁ * q₂).num = q₁.num * q₂.num / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

theorem NNRat.mul_den (q₁ q₂ : ℚ≥0) : (q₁ * q₂).den = q₁.den * q₂.den / (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

theorem NNRat.den_mul_den_eq_den_mul_gcd (q₁ q₂ : ℚ≥0) : q₁.den * q₂.den = (q₁ * q₂).den * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

A version of NNRat.mul_den without division.

theorem NNRat.num_mul_num_eq_num_mul_gcd (q₁ q₂ : ℚ≥0) : q₁.num * q₂.num = (q₁ * q₂).num * (q₁.num * q₂.num).gcd (q₁.den * q₂.den)

A version of NNRat.mul_num without division.