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.

source

def Nat.castAddMonoidHom (α : Type u_3) [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) }

Instances For

source

@[simp]

theorem Nat.coe_castAddMonoidHom {α : Type u_1} [AddMonoidWithOne α] :

⇑(Nat.castAddMonoidHom α) = Nat.cast

source

@[simp]

theorem Nat.cast_mul {α : Type u_1} [NonAssocSemiring α] (m : ℕ) (n : ℕ) :

↑(m * n) = ↑m * ↑n

source

def Nat.castRingHom (α : Type u_3) [NonAssocSemiring α] :

ℕ →+* α

Nat.cast : ℕ → α as a RingHom

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Nat.coe_castRingHom {α : Type u_1} [NonAssocSemiring α] :

⇑(Nat.castRingHom α) = Nat.cast

source

theorem Nat.coe_nat_dvd {α : Type u_1} [Semiring α] {m : ℕ} {n : ℕ} (h : m ∣ n) :

↑m ∣ ↑n

source

theorem Dvd.dvd.natCast {α : Type u_1} [Semiring α] {m : ℕ} {n : ℕ} (h : m ∣ n) :

↑m ∣ ↑n

Alias of Nat.coe_nat_dvd.

source

theorem ext_nat' {A : Type u_3} {F : Type u_5} [AddMonoid A] [AddMonoidHomClass F ℕ A] (f : F) (g : F) (h : f 1 = g 1) :

f = g

source

theorem AddMonoidHom.ext_nat {A : Type u_3} [AddMonoid A] {f : ℕ →+ A} {g : ℕ →+ A} :

f 1 = g 1 → f = g

source

theorem eq_natCast' {A : Type u_3} {F : Type u_5} [AddMonoidWithOne A] [AddMonoidHomClass F ℕ A] (f : F) (h1 : f 1 = 1) (n : ℕ) :

f n = ↑n

source

theorem map_natCast' {B : Type u_4} {F : Type u_5} [AddMonoidWithOne B] {A : Type u_6} [AddMonoidWithOne A] [AddMonoidHomClass F A B] (f : F) (h : f 1 = 1) (n : ℕ) :

f ↑n = ↑n

source

theorem ext_nat'' {A : Type u_3} {F : Type u_4} [MulZeroOneClass A] [MonoidWithZeroHomClass F ℕ A] (f : F) (g : F) (h_pos : ∀ {n : ℕ}, 0 < n → f n = g n) :

f = g

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

source

theorem MonoidWithZeroHom.ext_nat {A : Type u_3} [MulZeroOneClass A] {f : ℕ →*₀ A} {g : ℕ →*₀ A} :

(∀ {n : ℕ}, 0 < n → f n = g n) → f = g

source

@[simp]

theorem eq_natCast {R : Type u_3} {F : Type u_5} [NonAssocSemiring R] [RingHomClass F ℕ R] (f : F) (n : ℕ) :

f n = ↑n

source

@[simp]

theorem map_natCast {R : Type u_3} {S : Type u_4} {F : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [RingHomClass F R S] (f : F) (n : ℕ) :

f ↑n = ↑n

source

@[simp]

theorem map_ofNat {R : Type u_3} {S : Type u_4} {F : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [RingHomClass F R S] (f : F) (n : ℕ) [Nat.AtLeastTwo n] :

f (OfNat.ofNat n) = OfNat.ofNat n

source

theorem ext_nat {R : Type u_3} {F : Type u_5} [NonAssocSemiring R] [RingHomClass F ℕ R] (f : F) (g : F) :

f = g

source

theorem NeZero.nat_of_neZero {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] {F : Type u_8} [RingHomClass F R S] (f : F) {n : ℕ} [hn : NeZero ↑n] :

NeZero ↑n

source

theorem RingHom.eq_natCast' {R : Type u_3} [NonAssocSemiring R] (f : ℕ →+* R) :

f = Nat.castRingHom R

This is primed to match eq_intCast'.

source

@[simp]

theorem Nat.cast_id (n : ℕ) :

↑n = n

source

@[simp]

theorem Nat.castRingHom_nat :

Nat.castRingHom ℕ = RingHom.id ℕ

source

instance Nat.uniqueRingHom {R : Type u_3} [NonAssocSemiring R] :

Unique (ℕ →+* R)

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

Equations

Nat.uniqueRingHom = { toInhabited := { default := Nat.castRingHom R }, uniq := (_ : ∀ (f : ℕ →+* R), f = Nat.castRingHom R) }

source

instance Pi.natCast {α : Type u_1} {π : α → Type u_3} [(a : α) → NatCast (π a)] :

NatCast ((a : α) → π a)

Equations

Pi.natCast = { natCast := fun (n : ℕ) (x : α) => ↑n }

source

theorem Pi.nat_apply {α : Type u_1} {π : α → Type u_3} [(a : α) → NatCast (π a)] (n : ℕ) (a : α) :

↑n a = ↑n

source

@[simp]

theorem Pi.coe_nat {α : Type u_1} {π : α → Type u_3} [(a : α) → NatCast (π a)] (n : ℕ) :

↑n = fun (x : α) => ↑n

source

@[simp]

theorem Pi.ofNat_apply {α : Type u_1} {π : α → Type u_3} [(a : α) → NatCast (π a)] (n : ℕ) [Nat.AtLeastTwo n] (a : α) :

OfNat.ofNat n a = ↑n

source

theorem Sum.elim_natCast_natCast {α : Type u_3} {β : Type u_4} {γ : Type u_5} [NatCast γ] (n : ℕ) :

Sum.elim ↑n ↑n = ↑n