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) [AddMonoidWithOne α] : ℕ →+ α

Nat.cast : ℕ → α as an AddMonoidHom.

Equations

• Nat.castAddMonoidHom α = { toFun := Nat.cast, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Nat.coe_castAddMonoidHom {α : Type u_1} [AddMonoidWithOne α] : ⇑(castAddMonoidHom α) = Nat.cast

theorem Even.natCast {α : Type u_1} [AddMonoidWithOne α] {n : ℕ} (hn : Even n) : Even ↑n

@[simp]

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

def Nat.castRingHom (α : Type u_1) [NonAssocSemiring α] : ℕ →+* α

Nat.cast : ℕ → α as a RingHom

Equations

• Nat.castRingHom α = { toFun := Nat.cast, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Nat.coe_castRingHom {α : Type u_1} [NonAssocSemiring α] : ⇑(castRingHom α) = Nat.cast

theorem nsmul_eq_mul' {α : Type u_1} [NonAssocSemiring α] (a : α) (n : ℕ) : n • a = a * ↑n

@[simp]

theorem nsmul_eq_mul {α : Type u_1} [NonAssocSemiring α] (n : ℕ) (a : α) : n • a = ↑n * a

@[simp]

theorem Nat.cast_pow {α : Type u_1} [Semiring α] (m n : ℕ) : ↑(m ^ n) = ↑m ^ n

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

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

Alias of Nat.cast_dvd_cast.

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

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

theorem map_ofNat' {B : Type u_4} {F : Type u_5} [AddMonoidWithOne B] {A : Type u_6} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B] (f : F) (h : f 1 = 1) (n : ℕ) [n.AtLeastTwo] : f (OfNat.ofNat n) = OfNat.ofNat n

theorem ext_nat'' {A : Type u_3} {F : Type u_4} [MulZeroOneClass A] [FunLike F ℕ A] [ZeroHomClass F ℕ A] (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.

theorem MonoidWithZeroHom.ext_nat {A : Type u_3} [MulZeroOneClass A] {f g : ℕ →*₀ A} : (∀ {n : ℕ}, 0 < n → f n = g n) → f = g

theorem MonoidWithZeroHom.ext_nat_iff {A : Type u_3} [MulZeroOneClass A] {f g : ℕ →*₀ A} : f = g ↔ ∀ {n : ℕ}, 0 < n → f n = g n

@[simp]

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

@[simp]

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

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

This lemma is not marked @[simp] lemma because its #discr_tree_key (for the LHS) would just be DFunLike.coe _ _, due to the ofNat that https://github.com/leanprover/lean4/issues/2867 forces us to include, and therefore it would negatively impact performance.

If that issue is resolved, this can be marked @[simp].

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

theorem NeZero.nat_of_neZero {R : Type u_6} {S : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] {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} [NonAssocSemiring R] (f : ℕ →+* R) : f = Nat.castRingHom R

This is primed to match eq_intCast'.

@[simp]

theorem Nat.cast_id (n : ℕ) : ↑n = n

@[simp]

theorem Nat.castRingHom_nat : castRingHom ℕ = RingHom.id ℕ

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 = { default := Nat.castRingHom R, uniq := ⋯ }

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

Equations

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

@[simp]

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

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

@[instance 100]

instance Pi.instOfNat {α : Type u_1} {π : α → Type u_3} (n : ℕ) [(i : α) → OfNat (π i) n] : OfNat ((i : α) → π i) n

Equations

• Pi.instOfNat n = { ofNat := fun (x : α) => OfNat.ofNat n }

@[simp]

theorem Pi.ofNat_apply {α : Type u_1} {π : α → Type u_3} (n : ℕ) [(i : α) → OfNat (π i) n] (a : α) : (OfNat.ofNat n) a = OfNat.ofNat n

theorem Pi.ofNat_def {α : Type u_1} {π : α → Type u_3} (n : ℕ) [(i : α) → OfNat (π i) n] : OfNat.ofNat n = fun (x : α) => OfNat.ofNat n

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