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 α = { toZeroHom := { toFun := Nat.cast, map_zero' := (_ : ↑0 = 0) }, map_add' := (_ : ∀ (m n : ℕ), ↑(m + n) = ↑m + ↑n) }

@[simp]

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

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

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

@[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.coe_nat_dvd {α : 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.coe_nat_dvd.

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

theorem AddMonoidHom.ext_nat {A : Type u_3} [AddMonoid A] {f : ℕ →+ A} {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

@[simp]

theorem nsmul_one {A : Type u_6} [AddMonoidWithOne A] (n : ℕ) : n • 1 = ↑n

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

theorem MonoidWithZeroHom.ext_nat {A : Type u_3} [MulZeroOneClass A] {f : ℕ →*₀ A} {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

@[simp]

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 : ℕ) [Nat.AtLeastTwo n] : f (OfNat.ofNat n) = OfNat.ofNat n

theorem ext_nat {R : Type u_3} {F : Type u_5} [NonAssocSemiring R] [FunLike F ℕ R] [RingHomClass F ℕ R] (f : 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 = { toInhabited := { default := Nat.castRingHom R }, uniq := (_ : ∀ (f : ℕ →+* R), f = Nat.castRingHom R) }

def multiplesHom (α : Type u_1) [AddMonoid α] : α ≃ (ℕ →+ α)

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

Equations

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

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_1} [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_1} [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 : Multiplicative ℕ →* α⦄ ⦃g : Multiplicative ℕ →* α⦄ (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g

theorem AddMonoidHom.apply_nat {α : Type u_1} [AddMonoid α] (f : ℕ →+ α) (n : ℕ) : f n = n • f 1

def multiplesAddHom (α : Type u_1) [AddCommMonoid α] : α ≃+ (ℕ →+ α)

If α is commutative, multiplesHom is an additive equivalence.

Equations

• multiplesAddHom α = let src := multiplesHom α; { toEquiv := src, map_add' := (_ : ∀ (a b : α), (multiplesHom α).toFun (a + b) = (multiplesHom α).toFun a + (multiplesHom α).toFun b) }

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

If α is commutative, powersHom is a multiplicative equivalence.

Equations

• powersMulHom α = let src := powersHom α; { toEquiv := src, map_mul' := (_ : ∀ (a b : α), (powersHom α).toFun (a * b) = (powersHom α).toFun a * (powersHom α).toFun b) }

@[simp]

theorem multiplesAddHom_apply (α : Type u_1) [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_1) [AddCommMonoid α] (f : ℕ →+ α) : (AddEquiv.symm (multiplesAddHom α)) f = f 1

@[simp]

theorem powersMulHom_symm_apply (α : Type u_1) [CommMonoid α] (f : Multiplicative ℕ →* α) : (MulEquiv.symm (powersMulHom α)) f = f (Multiplicative.ofAdd 1)

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

Equations

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

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

@[simp]

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

@[simp]

theorem Pi.ofNat_apply {α : Type u_1} {π : α → Type u_3} [(a : α) → NatCast (π a)] (n : ℕ) [Nat.AtLeastTwo n] (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