Documentation

Mathlib.Data.Nat.Cast.Basic

Cast of natural numbers (additional theorems) #

This file proves additional properties about the canonical homomorphism from the natural numbers into an additive monoid with a one (Nat.cast).

Main declarations #

def Nat.castAddMonoidHom (α : Type u_1) [inst : AddMonoidWithOne α] :

Nat.cast : ℕ → α→ α as an AddMonoidHom.

Equations
  • Nat.castAddMonoidHom α = { toZeroHom := { toFun := Nat.cast, map_zero' := (_ : 0 = 0) }, map_add' := (_ : ∀ (m n : ), ↑(m + n) = m + n) }
@[simp]
theorem Nat.coe_castAddMonoidHom {α : Type u_1} [inst : AddMonoidWithOne α] :
↑(Nat.castAddMonoidHom α) = Nat.cast
@[simp]
theorem Nat.cast_mul {α : Type u_1} [inst : NonAssocSemiring α] (m : ) (n : ) :
↑(m * n) = m * n
def Nat.castRingHom (α : Type u_1) [inst : NonAssocSemiring α] :

Nat.cast : ℕ → α→ α as a RingHom

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Nat.coe_castRingHom {α : Type u_1} [inst : NonAssocSemiring α] :
↑(Nat.castRingHom α) = Nat.cast
theorem Nat.cast_commute {α : Type u_1} [inst : NonAssocSemiring α] (n : ) (x : α) :
Commute (n) x
theorem Nat.cast_comm {α : Type u_1} [inst : NonAssocSemiring α] (n : ) (x : α) :
n * x = x * n
theorem Nat.commute_cast {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ) :
Commute x n
theorem Nat.mono_cast {α : Type u_1} [inst : OrderedSemiring α] :
Monotone Nat.cast
@[simp]
theorem Nat.cast_nonneg {α : Type u_1} [inst : OrderedSemiring α] (n : ) :
0 n
theorem Nat.cast_add_one_pos {α : Type u_1} [inst : OrderedSemiring α] [inst : Nontrivial α] (n : ) :
0 < n + 1
@[simp]
theorem Nat.cast_pos {α : Type u_1} [inst : OrderedSemiring α] [inst : Nontrivial α] {n : } :
0 < n 0 < n
theorem Nat.strictMono_cast {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] :
StrictMono Nat.cast
@[simp]
theorem Nat.castOrderEmbedding_apply {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] :
Nat.castOrderEmbedding.toEmbedding = Nat.cast
def Nat.castOrderEmbedding {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] :

Nat.cast : ℕ → α→ α as an OrderEmbedding

Equations
@[simp]
theorem Nat.cast_le {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {m : } {n : } :
m n m n
@[simp]
theorem Nat.cast_lt {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {m : } {n : } :
m < n m < n
@[simp]
theorem Nat.one_lt_cast {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {n : } :
1 < n 1 < n
@[simp]
theorem Nat.one_le_cast {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {n : } :
1 n 1 n
@[simp]
theorem Nat.cast_lt_one {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {n : } :
n < 1 n = 0
@[simp]
theorem Nat.cast_le_one {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {n : } :
n 1 n 1
@[simp]
theorem Nat.cast_tsub {α : Type u_1} [inst : CanonicallyOrderedCommSemiring α] [inst : Sub α] [inst : OrderedSub α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (m : ) (n : ) :
↑(m - n) = m - n

A version of Nat.cast_sub that works for ℝ≥0≥0 and ℚ≥0≥0. Note that this proof doesn't work for ℕ∞∞ and ℝ≥0∞≥0∞∞, so we use type-specific lemmas for these types.

@[simp]
theorem Nat.cast_min {α : Type u_1} [inst : LinearOrderedSemiring α] {a : } {b : } :
↑(min a b) = min a b
@[simp]
theorem Nat.cast_max {α : Type u_1} [inst : LinearOrderedSemiring α] {a : } {b : } :
↑(max a b) = max a b
@[simp]
theorem Nat.abs_cast {α : Type u_1} [inst : LinearOrderedRing α] (a : ) :
abs a = a
theorem Nat.coe_nat_dvd {α : Type u_1} [inst : Semiring α] {m : } {n : } (h : m n) :
m n
theorem Dvd.dvd.natCast {α : Type u_1} [inst : Semiring α] {m : } {n : } (h : m n) :
m n

Alias of Nat.coe_nat_dvd.

theorem ext_nat' {A : Type u_1} {F : Type u_2} [inst : AddMonoid A] [inst : AddMonoidHomClass F A] (f : F) (g : F) (h : f 1 = g 1) :
f = g
theorem AddMonoidHom.ext_nat {A : Type u_1} [inst : AddMonoid A] {f : →+ A} {g : →+ A} :
f 1 = g 1f = g
theorem eq_natCast' {A : Type u_2} {F : Type u_1} [inst : AddMonoidWithOne A] [inst : AddMonoidHomClass F A] (f : F) (h1 : f 1 = 1) (n : ) :
f n = n
theorem map_natCast' {B : Type u_3} {F : Type u_2} [inst : AddMonoidWithOne B] {A : Type u_1} [inst : AddMonoidWithOne A] [inst : AddMonoidHomClass F A B] (f : F) (h : f 1 = 1) (n : ) :
f n = n
theorem ext_nat'' {A : Type u_2} {F : Type u_1} [inst : MulZeroOneClass A] [inst : MonoidWithZeroHomClass F A] (f : F) (g : F) (h_pos : ∀ {n : }, 0 < nf n = g n) :
f = g

If two MonoidWithZeroHoms agree on the positive naturals they are equal.

theorem MonoidWithZeroHom.ext_nat {A : Type u_1} [inst : MulZeroOneClass A] {f : →*₀ A} {g : →*₀ A} :
(∀ {n : }, 0 < nf n = g n) → f = g
@[simp]
theorem eq_natCast {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst : RingHomClass F R] (f : F) (n : ) :
f n = n
@[simp]
theorem map_natCast {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : RingHomClass F R S] (f : F) (n : ) :
f n = n
theorem ext_nat {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst : RingHomClass F R] (f : F) (g : F) :
f = g
theorem NeZero.nat_of_injective {R : Type u_1} {S : Type u_3} {F : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {n : } [h : NeZero n] [inst : RingHomClass F R S] {f : F} (hf : Function.Injective f) :
NeZero n
theorem NeZero.nat_of_neZero {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] {F : Type u_3} [inst : RingHomClass F R S] (f : F) {n : } [hn : NeZero n] :
NeZero n
theorem RingHom.eq_natCast' {R : Type u_1} [inst : NonAssocSemiring R] (f : →+* R) :

This is primed to match eq_intCast'.

@[simp]
theorem Nat.cast_id (n : ) :
n = n
instance Nat.uniqueRingHom {R : Type u_1} [inst : NonAssocSemiring R] :

We don't use RingHomClass here, since that might cause type-class slowdown for Subsingleton

Equations
instance Pi.natCast {α : Type u_1} {π : αType u_2} [inst : (a : α) → NatCast (π a)] :
NatCast ((a : α) → π a)
Equations
  • Pi.natCast = { natCast := fun n x => n }
theorem Pi.nat_apply {α : Type u_2} {π : αType u_1} [inst : (a : α) → NatCast (π a)] (n : ) (a : α) :
n a = n
@[simp]
theorem Pi.coe_nat {α : Type u_1} {π : αType u_2} [inst : (a : α) → NatCast (π a)] (n : ) :
n = fun x => n
theorem Sum.elim_natCast_natCast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : NatCast γ] (n : ) :
Sum.elim n n = n

Order dual #

instance instNatCastOrderDual {α : Type u_1} [h : NatCast α] :
Equations
  • instNatCastOrderDual = h
Equations
  • instAddMonoidWithOneOrderDual = h
Equations
  • instAddCommMonoidWithOneOrderDual = h
@[simp]
theorem toDual_natCast {α : Type u_1} [inst : NatCast α] (n : ) :
OrderDual.toDual n = n
@[simp]
theorem ofDual_natCast {α : Type u_1} [inst : NatCast α] (n : ) :
↑(OrderDual.ofDual n) = n

Lexicographic order #

instance instNatCastLex {α : Type u_1} [h : NatCast α] :
Equations
  • instNatCastLex = h
Equations
  • instAddMonoidWithOneLex = h
Equations
  • instAddCommMonoidWithOneLex = h
@[simp]
theorem toLex_natCast {α : Type u_1} [inst : NatCast α] (n : ) :
toLex n = n
@[simp]
theorem ofLex_natCast {α : Type u_1} [inst : NatCast α] (n : ) :
↑(ofLex n) = n