Cast of naturals into fields #
This file concerns the canonical homomorphism ℕ → F, where F is a field.
Main results #
Nat.cast_div: ifndividesm, then↑(m / n) = ↑m / ↑n
@[simp]
theorem
Nat.cast_div
{K : Type u_1}
[DivisionSemiring K]
{m n : ℕ}
(hnm : n ∣ m)
(hn : ↑n ≠ 0)
:
↑(m / n) = ↑m / ↑n
@[simp]
theorem
Nat.cast_div_charZero
{K : Type u_1}
[DivisionSemiring K]
{m n : ℕ}
[CharZero K]
(hnm : n ∣ m)
:
↑(m / n) = ↑m / ↑n
theorem
Nat.cast_div_div_div_cancel_right
{K : Type u_1}
[DivisionSemiring K]
{d m n : ℕ}
[CharZero K]
(hn : d ∣ n)
(hm : d ∣ m)
:
↑(m / d) / ↑(n / d) = ↑m / ↑n