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

ink

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

source

ink

@[simp]

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

↑(Nat.castAddMonoidHom α) = Nat.cast

source

ink

@[simp]

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

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

source

ink

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

ℕ →+* α

Nat.cast : ℕ → α→ α as a RingHom

Equations

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

source

ink

@[simp]

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

↑(Nat.castRingHom α) = Nat.cast

source

ink

theorem Nat.cast_commute {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α) :

Commute (↑n) x

source

ink

theorem Nat.cast_comm {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α) :

↑n * x = x * ↑n

source

ink

theorem Nat.commute_cast {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ℕ) :

Commute x ↑n

source

ink

theorem Nat.mono_cast {α : Type u_1} [inst : OrderedSemiring α] :

Monotone Nat.cast

source

ink

@[simp]

theorem Nat.cast_nonneg {α : Type u_1} [inst : OrderedSemiring α] (n : ℕ) :

0 ≤ ↑n

source

ink

theorem Nat.cast_add_one_pos {α : Type u_1} [inst : OrderedSemiring α] [inst : Nontrivial α] (n : ℕ) :

0 < ↑n + 1

source

ink

@[simp]

theorem Nat.cast_pos {α : Type u_1} [inst : OrderedSemiring α] [inst : Nontrivial α] {n : ℕ} :

0 < ↑n ↔ 0 < n

source

ink

theorem Nat.strictMono_cast {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] :

StrictMono Nat.cast

source

ink

@[simp]

theorem Nat.castOrderEmbedding_apply {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] :

↑Nat.castOrderEmbedding.toEmbedding = Nat.cast

source

ink

def Nat.castOrderEmbedding {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] :

ℕ ↪o α

Nat.cast : ℕ → α→ α as an OrderEmbedding

Equations

Nat.castOrderEmbedding = OrderEmbedding.ofStrictMono Nat.cast (_ : StrictMono Nat.cast)

source

ink

@[simp]

theorem Nat.cast_le {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {m : ℕ} {n : ℕ} :

↑m ≤ ↑n ↔ m ≤ n

source

ink

@[simp]

theorem Nat.cast_lt {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {m : ℕ} {n : ℕ} :

↑m < ↑n ↔ m < n

source

ink

@[simp]

theorem Nat.one_lt_cast {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {n : ℕ} :

1 < ↑n ↔ 1 < n

source

ink

@[simp]

theorem Nat.one_le_cast {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {n : ℕ} :

1 ≤ ↑n ↔ 1 ≤ n

source

ink

@[simp]

theorem Nat.cast_lt_one {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {n : ℕ} :

↑n < 1 ↔ n = 0

source

ink

@[simp]

theorem Nat.cast_le_one {α : Type u_1} [inst : OrderedSemiring α] [inst : CharZero α] {n : ℕ} :

↑n ≤ 1 ↔ n ≤ 1

source

ink

@[simp]

theorem Nat.cast_tsub {α : Type u_1} [inst : CanonicallyOrderedCommSemiring α] [inst : Sub α] [inst : OrderedSub α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (m : ℕ) (n : ℕ) :

↑(m - n) = ↑m - ↑n

A version of Nat.cast_sub that works for ℝ≥0≥0 and ℚ≥0≥0. Note that this proof doesn't work for ℕ∞∞ and ℝ≥0∞≥0∞∞, so we use type-specific lemmas for these types.

source

ink

@[simp]

theorem Nat.cast_min {α : Type u_1} [inst : LinearOrderedSemiring α] {a : ℕ} {b : ℕ} :

↑(min a b) = min ↑a ↑b

source

ink

@[simp]

theorem Nat.cast_max {α : Type u_1} [inst : LinearOrderedSemiring α] {a : ℕ} {b : ℕ} :

↑(max a b) = max ↑a ↑b

source

ink

@[simp]

theorem Nat.abs_cast {α : Type u_1} [inst : LinearOrderedRing α] (a : ℕ) :

abs ↑a = ↑a

source

ink

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

↑m ∣ ↑n

source

ink

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

↑m ∣ ↑n

Alias of Nat.coe_nat_dvd.

source

ink

instance instNontrivial {α : Type u_1} [inst : AddMonoidWithOne α] [inst : CharZero α] :

Nontrivial α

Equations

@instNontrivial = @instNontrivial.proof_1

source

ink

theorem ext_nat' {A : Type u_1} {F : Type u_2} [inst : AddMonoid A] [inst : AddMonoidHomClass F ℕ A] (f : F) (g : F) (h : ↑f 1 = ↑g 1) :

f = g

source

ink

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

↑f 1 = ↑g 1 → f = g

source

ink

theorem eq_natCast' {A : Type u_2} {F : Type u_1} [inst : AddMonoidWithOne A] [inst : AddMonoidHomClass F ℕ A] (f : F) (h1 : ↑f 1 = 1) (n : ℕ) :

↑f n = ↑n

source

ink

theorem map_natCast' {B : Type u_3} {F : Type u_2} [inst : AddMonoidWithOne B] {A : Type u_1} [inst : AddMonoidWithOne A] [inst : AddMonoidHomClass F A B] (f : F) (h : ↑f 1 = 1) (n : ℕ) :

↑f ↑n = ↑n

source

ink

theorem ext_nat'' {A : Type u_2} {F : Type u_1} [inst : MulZeroOneClass A] [inst : 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

ink

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

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

source

ink

@[simp]

theorem eq_natCast {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst : RingHomClass F ℕ R] (f : F) (n : ℕ) :

↑f n = ↑n

source

ink

@[simp]

theorem map_natCast {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : RingHomClass F R S] (f : F) (n : ℕ) :

↑f ↑n = ↑n

source

ink

theorem ext_nat {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst : RingHomClass F ℕ R] (f : F) (g : F) :

f = g

source

ink

theorem NeZero.nat_of_injective {R : Type u_1} {S : Type u_3} {F : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] {n : ℕ} [h : NeZero ↑n] [inst : RingHomClass F R S] {f : F} (hf : Function.Injective ↑f) :

NeZero ↑n

source

ink

theorem NeZero.nat_of_neZero {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] {F : Type u_3} [inst : RingHomClass F R S] (f : F) {n : ℕ} [hn : NeZero ↑n] :

NeZero ↑n

source

ink