divNat — Mathlib

English

Define the quotient n/d as a nonnegative rational number when n, d ∈ ℕ.

Русский

Определим частное n/d как неотрицательное рациональное число, когда n, d ∈ ℕ.

LaTeX

$$$ \mathrm{divNat}(n,d) \;\text{is the nonnegative rational } \frac{n}{d} $$$

Lean4

/-- Form the quotient `n / d` where `n d : ℕ`.

See also `Rat.divInt` and `mkRat`. -/
def divNat (n d : ℕ) : ℚ≥0 :=
  ⟨.divInt n d, Rat.divInt_nonneg (Int.ofNat_zero_le n) (Int.ofNat_zero_le d)⟩

Похожие утверждения