# 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 #

• castAddMonoidHom: cast bundled as an AddMonoidHom.
• castRingHom: cast bundled as a RingHom.
def Nat.castAddMonoidHom (α : Type u_3) [] :

Nat.cast : ℕ → α as an AddMonoidHom.

Equations
• = { toFun := Nat.cast, map_zero' := , map_add' := }
Instances For
@[simp]
theorem Nat.coe_castAddMonoidHom {α : Type u_1} [] :
= Nat.cast
theorem Even.natCast {α : Type u_1} [] {n : } (hn : Even n) :
Even n
@[simp]
theorem Nat.cast_mul {α : Type u_1} [] (m : ) (n : ) :
(m * n) = m * n
def Nat.castRingHom (α : Type u_1) [] :

Nat.cast : ℕ → α as a RingHom

Equations
• = let __src := ; { toFun := Nat.cast, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Nat.coe_castRingHom {α : Type u_1} [] :
() = Nat.cast
theorem nsmul_eq_mul' {α : Type u_1} [] (a : α) (n : ) :
n a = a * n
@[simp]
theorem nsmul_eq_mul {α : Type u_1} [] (n : ) (a : α) :
n a = n * a
@[simp]
theorem Nat.cast_pow {α : Type u_1} [] (m : ) (n : ) :
(m ^ n) = m ^ n
theorem Nat.cast_dvd_cast {α : Type u_1} [] {m : } {n : } (h : m n) :
m n
theorem Dvd.dvd.natCast {α : Type u_1} [] {m : } {n : } (h : m n) :
m n

Alias of Nat.cast_dvd_cast.

theorem ext_nat' {A : Type u_3} {F : Type u_5} [FunLike F A] [] [] (f : F) (g : F) (h : f 1 = g 1) :
f = g
theorem AddMonoidHom.ext_nat {A : Type u_3} [] {f : →+ A} {g : →+ A} :
f 1 = g 1f = g
theorem eq_natCast' {A : Type u_3} {F : Type u_5} [FunLike F A] [] [] (f : F) (h1 : f 1 = 1) (n : ) :
f n = n
theorem map_natCast' {B : Type u_4} {F : Type u_5} [] {A : Type u_6} [] [FunLike F A B] [] (f : F) (h : f 1 = 1) (n : ) :
f n = n
theorem map_ofNat' {B : Type u_4} {F : Type u_5} [] {A : Type u_6} [] [FunLike F A B] [] (f : F) (h : f 1 = 1) (n : ) [n.AtLeastTwo] :
f () =
@[simp]
theorem nsmul_one {A : Type u_6} [] (n : ) :
n 1 = n
theorem ext_nat'' {A : Type u_3} {F : Type u_4} [] [FunLike 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_3} [] {f : →*₀ A} {g : →*₀ A} :
(∀ {n : }, 0 < nf n = g n)f = g
@[simp]
theorem eq_natCast {R : Type u_3} {F : Type u_5} [] [FunLike F R] [] (f : F) (n : ) :
f n = n
@[simp]
theorem map_natCast {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F R S] [RingHomClass F R S] (f : F) (n : ) :
f n = n
@[simp]
theorem map_ofNat {R : Type u_3} {S : Type u_4} {F : Type u_5} [] [] [FunLike F R S] [RingHomClass F R S] (f : F) (n : ) [n.AtLeastTwo] :
f () =
theorem ext_nat {R : Type u_3} {F : Type u_5} [] [FunLike F R] [] (f : F) (g : F) :
f = g
theorem NeZero.nat_of_neZero {R : Type u_6} {S : Type u_7} [] [] {F : Type u_8} [FunLike F R S] [RingHomClass F R S] (f : F) {n : } [hn : NeZero n] :
NeZero n
theorem RingHom.eq_natCast' {R : Type u_3} [] (f : →+* R) :

This is primed to match eq_intCast'.

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

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

Equations
• Nat.uniqueRingHom = { default := , uniq := }
def multiplesHom (β : Type u_2) [] :
β ( →+ β)

Additive homomorphisms from ℕ are defined by the image of 1.

Equations
• = { toFun := fun (x : β) => { toFun := fun (n : ) => n x, map_zero' := , map_add' := }, invFun := fun (f : →+ β) => f 1, left_inv := , right_inv := }
Instances For
def powersHom (α : Type u_1) [] :
α ()

Monoid homomorphisms from Multiplicative ℕ are defined by the image of Multiplicative.ofAdd 1.

Equations
Instances For
@[simp]
theorem multiplesHom_apply (β : Type u_2) [] (x : β) (n : ) :
(() x) n = n x
@[simp]
theorem powersHom_apply {α : Type u_1} [] (x : α) (n : ) :
(() x) n = x ^ Multiplicative.toAdd n
@[simp]
theorem multiplesHom_symm_apply (β : Type u_2) [] (f : →+ β) :
().symm f = f 1
@[simp]
theorem powersHom_symm_apply {α : Type u_1} [] (f : ) :
().symm f = f (Multiplicative.ofAdd 1)
theorem MonoidHom.apply_mnat {α : Type u_1} [] (f : ) (n : ) :
theorem MonoidHom.ext_mnat {α : Type u_1} [] ⦃f : ⦃g : (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) :
f = g
theorem AddMonoidHom.apply_nat (β : Type u_2) [] (f : →+ β) (n : ) :
f n = n f 1
def multiplesAddHom (β : Type u_2) [] :
β ≃+ ( →+ β)

If α is commutative, multiplesHom is an additive equivalence.

Equations
• = let __src := ; { toEquiv := __src, map_add' := }
Instances For
def powersMulHom (α : Type u_1) [] :
α ≃* ()

If α is commutative, powersHom is a multiplicative equivalence.

Equations
• = let __src := ; { toEquiv := __src, map_mul' := }
Instances For
@[simp]
theorem multiplesAddHom_apply (β : Type u_2) [] (x : β) (n : ) :
(() x) n = n x
@[simp]
theorem powersMulHom_apply (α : Type u_1) [] (x : α) (n : ) :
(() x) n = x ^ Multiplicative.toAdd n
@[simp]
theorem multiplesAddHom_symm_apply (β : Type u_2) [] (f : →+ β) :
().symm f = f 1
@[simp]
theorem powersMulHom_symm_apply (α : Type u_1) [] (f : ) :
().symm f = f (Multiplicative.ofAdd 1)
instance Pi.instNatCast {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] :
NatCast ((a : α) → π a)
Equations
• Pi.instNatCast = { natCast := fun (n : ) (x : α) => n }
theorem Pi.natCast_apply {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) (a : α) :
n a = n
@[simp]
theorem Pi.natCast_def {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) :
n = fun (x : α) => n
@[deprecated Pi.natCast_apply]
theorem Pi.nat_apply {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) (a : α) :
n a = n

Alias of Pi.natCast_apply.

@[deprecated Pi.natCast_def]
theorem Pi.coe_nat {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) :
n = fun (x : α) => n

Alias of Pi.natCast_def.

@[simp]
theorem Pi.ofNat_apply {α : Type u_1} {π : αType u_3} [(a : α) → NatCast (π a)] (n : ) [n.AtLeastTwo] (a : α) :
= n
theorem Sum.elim_natCast_natCast {α : Type u_3} {β : Type u_4} {γ : Type u_5} [] (n : ) :
Sum.elim n n = n