Documentation

Mathlib.Data.Nat.Cast.Field

Cast of naturals into fields #

This file concerns the canonical homomorphism ℕ → F, where F is a field.

Main results #

@[simp]
theorem Nat.cast_div {α : Type u_1} [DivisionSemiring α] {m : } {n : } (n_dvd : n m) (hn : n 0) :
(m / n) = m / n
theorem Nat.cast_div_div_div_cancel_right {α : Type u_1} [DivisionSemiring α] [CharZero α] {m : } {n : } {d : } (hn : d n) (hm : d m) :
(m / d) / (n / d) = m / n