mathlib3 documentation

data.nat.cast.field

Cast of naturals into fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main results #

@[simp]
theorem nat.cast_div {α : Type u_1} [division_semiring α] {m n : } (n_dvd : n m) (n_nonzero : n 0) :
(m / n) = m / n
theorem nat.cast_div_div_div_cancel_right {α : Type u_1} [division_semiring α] [char_zero α] {m n d : } (hn : d n) (hm : d m) :
(m / d) / (n / d) = m / n
theorem nat.cast_div_le {α : Type u_1} [linear_ordered_semifield α] {m n : } :
(m / n) m / n

Natural division is always less than division in the field.

theorem nat.inv_pos_of_nat {α : Type u_1} [linear_ordered_semifield α] {n : } :
0 < (n + 1)⁻¹
theorem nat.one_div_pos_of_nat {α : Type u_1} [linear_ordered_semifield α] {n : } :
0 < 1 / (n + 1)
theorem nat.one_div_le_one_div {α : Type u_1} [linear_ordered_semifield α] {n m : } (h : n m) :
1 / (m + 1) 1 / (n + 1)
theorem nat.one_div_lt_one_div {α : Type u_1} [linear_ordered_semifield α] {n m : } (h : n < m) :
1 / (m + 1) < 1 / (n + 1)