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 α] : ⇑(Nat.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 α] : ⇑(Nat.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 ext_nat' {A : Type u_3} {F : Type u_5} [FunLike F ℕ A] [AddMonoid A] [AddMonoidHomClass F ℕ A] (f g : F) (h : f 1 = g 1) : f = g

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

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] [MonoidWithZeroHomClass 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

@[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 no_index 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} [Semiring R] [Semiring 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 : 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 := ⋯ }

def multiplesHom (β : Type u_2) [AddMonoid β] : β ≃ (ℕ →+ β)

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

Equations

• multiplesHom β = { toFun := fun (x : β) => { toFun := fun (n : ℕ) => n • x, map_zero' := ⋯, map_add' := ⋯ }, invFun := fun (f : ℕ →+ β) => f 1, left_inv := ⋯, right_inv := ⋯ }

def powersHom (α : Type u_1) [Monoid α] : α ≃ (Multiplicative ℕ →* α)

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

Equations

• powersHom α = Additive.ofMul.trans ((multiplesHom (Additive α)).trans AddMonoidHom.toMultiplicative'')

@[simp]

theorem multiplesHom_apply (β : Type u_2) [AddMonoid β] (x : β) (n : ℕ) : ((multiplesHom β) x) n = n • x

@[simp]

theorem powersHom_apply {α : Type u_1} [Monoid α] (x : α) (n : Multiplicative ℕ) : ((powersHom α) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem multiplesHom_symm_apply (β : Type u_2) [AddMonoid β] (f : ℕ →+ β) : (multiplesHom β).symm f = f 1

@[simp]

theorem powersHom_symm_apply {α : Type u_1} [Monoid α] (f : Multiplicative ℕ →* α) : (powersHom α).symm f = f (Multiplicative.ofAdd 1)

theorem MonoidHom.apply_mnat {α : Type u_1} [Monoid α] (f : Multiplicative ℕ →* α) (n : Multiplicative ℕ) : f n = f (Multiplicative.ofAdd 1) ^ Multiplicative.toAdd n

theorem MonoidHom.ext_mnat {α : Type u_1} [Monoid α] ⦃f g : Multiplicative ℕ →* α⦄ (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g

theorem AddMonoidHom.apply_nat (β : Type u_2) [AddMonoid β] (f : ℕ →+ β) (n : ℕ) : f n = n • f 1

def multiplesAddHom (β : Type u_2) [AddCommMonoid β] : β ≃+ (ℕ →+ β)

If α is commutative, multiplesHom is an additive equivalence.

Equations

• multiplesAddHom β = { toEquiv := multiplesHom β, map_add' := ⋯ }

def powersMulHom (α : Type u_1) [CommMonoid α] : α ≃* (Multiplicative ℕ →* α)

If α is commutative, powersHom is a multiplicative equivalence.

Equations

• powersMulHom α = { toEquiv := powersHom α, map_mul' := ⋯ }

@[simp]

theorem multiplesAddHom_apply (β : Type u_2) [AddCommMonoid β] (x : β) (n : ℕ) : ((multiplesAddHom β) x) n = n • x

@[simp]

theorem powersMulHom_apply (α : Type u_1) [CommMonoid α] (x : α) (n : Multiplicative ℕ) : ((powersMulHom α) x) n = x ^ Multiplicative.toAdd n

@[simp]

theorem multiplesAddHom_symm_apply (β : Type u_2) [AddCommMonoid β] (f : ℕ →+ β) : (multiplesAddHom β).symm f = f 1

@[simp]

theorem powersMulHom_symm_apply (α : Type u_1) [CommMonoid α] (f : Multiplicative ℕ →* α) : (powersMulHom α).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 : α) : OfNat.ofNat n a = ↑n

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