Nat.cast_div
theorem Nat.cast_div : ∀ {α : Type u_1} [inst : DivisionSemiring α] {m n : ℕ}, n ∣ m → ↑n ≠ 0 → ↑(m / n) = ↑m / ↑n := by
sorry
This theorem, `Nat.cast_div`, states that for any type `α` that forms a division semiring, given natural numbers `m` and `n` such that `n` divides `m` and `n` is not zero, the casting of the division of `m` by `n` to type `α` is equal to the division of the castings of `m` and `n` to type `α`. In other words, if you divide `m` by `n` first and then cast the result to type `α`, you get the same result as if you cast `m` and `n` to `α` first and then perform the division.
More concisely: For any type `α` that forms a division semiring and natural numbers `m`, `n` with `n` dividing `m` non-zero, `(m / n).to α = m.to α / n.to α`.
|
Nat.cast_div_le
theorem Nat.cast_div_le : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {m n : ℕ}, ↑(m / n) ≤ ↑m / ↑n
This theorem states that for any linearly ordered semifield `α` and for any natural numbers `m` and `n`, the division of `m` by `n` in the natural number domain, when cast to `α`, is always less than or equal to the division of `m` by `n` in the field `α`. In other words, it asserts that casting the result of an integer division to a field is always less than or equal to performing the division within the field.
More concisely: For any linearly ordered semifield `α`, and natural numbers `m` and `n`, the cast of `m / n` from the natural number domain to `α` is less than or equal to `m / n` in `α`.
|