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 #

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' := ⋯ }

Instances For

@[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

@[instance_reducible]

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' := ⋯ }

Instances For

@[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

theorem Nat.ofNat_nsmul_eq_mul {α : Type u_1} [NonAssocSemiring α] (n : ℕ) [n.AtLeastTwo] (a : α) :

OfNat.ofNat n • a = OfNat.ofNat 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] :

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_reducible]

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_reducible, 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