Mathlib.Data.Nat.Cast.Basic

Nat.castAddMonoidHom definition

(α : Type*) [AddMonoidWithOne α] : ℕ →+ α

Full source

/-- `Nat.cast : ℕ → α` as an `AddMonoidHom`. -/
def castAddMonoidHom (α : Type*) [AddMonoidWithOne α] :
    ℕℕ →+ α where
  toFun := Nat.cast
  map_add' := cast_add
  map_zero' := cast_zero

Canonical homomorphism from naturals to additive monoid with one

Informal description

The canonical homomorphism from the natural numbers to an additive monoid with one $\alpha$, bundled as an additive monoid homomorphism. This homomorphism maps each natural number $n$ to its corresponding element in $\alpha$, preserves addition (i.e., $\text{cast}(m + n) = \text{cast}(m) + \text{cast}(n)$), and maps $0$ to the additive identity in $\alpha$.

Nat.coe_castAddMonoidHom theorem

[AddMonoidWithOne α] : (castAddMonoidHom α : ℕ → α) = Nat.cast

Full source

@[simp]
theorem coe_castAddMonoidHom [AddMonoidWithOne α] : (castAddMonoidHom α : ℕ → α) = Nat.cast :=
  rfl

Equality of Canonical Homomorphism and Natural Number Coercion

Informal description

For any additive monoid with one $\alpha$, the underlying function of the canonical additive monoid homomorphism from $\mathbb{N}$ to $\alpha$ is equal to the natural number coercion function $\text{Nat.cast}$.

Even.natCast theorem

[AddMonoidWithOne α] {n : ℕ} (hn : Even n) : Even (n : α)

Full source

lemma _root_.Even.natCast [AddMonoidWithOne α] {n : ℕ} (hn : Even n) : Even (n : α) :=
  hn.map <| Nat.castAddMonoidHom α

Evenness is preserved under the canonical homomorphism from naturals to an additive monoid with one

Informal description

For any additive monoid with one $\alpha$ and any even natural number $n$, the image of $n$ under the canonical homomorphism $\mathbb{N} \to \alpha$ is also even.

Nat.cast_mul theorem

(m n : ℕ) : ((m * n : ℕ) : α) = m * n

Full source

@[simp, norm_cast] lemma cast_mul (m n : ℕ) : ((m * n : ℕ) : α) = m * n := by
  induction n <;> simp [mul_succ, mul_add, *]

Canonical Homomorphism Preserves Multiplication: $\text{cast}(m \cdot n) = \text{cast}(m) \cdot \text{cast}(n)$

Informal description

For any additive monoid with one $\alpha$ and any natural numbers $m$ and $n$, the canonical homomorphism from $\mathbb{N}$ to $\alpha$ satisfies $\text{cast}(m \cdot n) = \text{cast}(m) \cdot \text{cast}(n)$.

Nat.castRingHom definition

: ℕ →+* α

Full source

/-- `Nat.cast : ℕ → α` as a `RingHom` -/
def castRingHom : ℕℕ →+* α :=
  { castAddMonoidHom α with toFun := Nat.cast, map_one' := cast_one, map_mul' := cast_mul }

Canonical ring homomorphism from naturals to a semiring

Informal description

The canonical homomorphism from the natural numbers $\mathbb{N}$ to a semiring $\alpha$, bundled as a ring homomorphism. This homomorphism maps each natural number $n$ to its corresponding element in $\alpha$, preserves addition and multiplication (i.e., $\text{cast}(m + n) = \text{cast}(m) + \text{cast}(n)$ and $\text{cast}(m \cdot n) = \text{cast}(m) \cdot \text{cast}(n)$), and maps $0$ and $1$ to the additive and multiplicative identities in $\alpha$ respectively.

Nat.coe_castRingHom theorem

: (castRingHom α : ℕ → α) = Nat.cast

Full source

@[simp, norm_cast] lemma coe_castRingHom : (castRingHom α : ℕ → α) = Nat.cast := rfl

Canonical Ring Homomorphism Equals Natural Number Cast

Informal description

The canonical ring homomorphism from the natural numbers $\mathbb{N}$ to a semiring $\alpha$, when viewed as a function, is equal to the natural number cast function $\text{Nat.cast}$.

nsmul_eq_mul' theorem

(a : α) (n : ℕ) : n • a = a * n

Full source

lemma _root_.nsmul_eq_mul' (a : α) (n : ℕ) : n • a = a * n := by
  induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, mul_zero]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, mul_add, mul_one]

Scalar Multiplication Equals Right Multiplication: $n \cdot a = a * n$

Informal description

For any element $a$ in a multiplicative monoid $\alpha$ and any natural number $n$, the $n$-th multiple of $a$ under scalar multiplication equals the product of $a$ and $n$, i.e., $n \cdot a = a * n$.

nsmul_eq_mul theorem

(n : ℕ) (a : α) : n • a = n * a

Full source

@[simp] lemma _root_.nsmul_eq_mul (n : ℕ) (a : α) : n • a = n * a := by
  induction n with
  | zero => rw [zero_nsmul, Nat.cast_zero, zero_mul]
  | succ n ih => rw [succ_nsmul, ih, Nat.cast_succ, add_mul, one_mul]

Scalar Multiplication Equals Left Multiplication: $n \cdot a = n * a$

Informal description

For any natural number $n$ and any element $a$ in a multiplicative monoid $\alpha$, the $n$-th multiple of $a$ under scalar multiplication equals the product of $n$ and $a$, i.e., $n \cdot a = n * a$.

Nat.cast_pow theorem

(m : ℕ) : ∀ n : ℕ, ↑(m ^ n) = (m ^ n : α)

Full source

@[simp, norm_cast]
lemma cast_pow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n) = (m ^ n : α)
  | 0 => by simp
  | n + 1 => by rw [_root_.pow_succ', _root_.pow_succ', cast_mul, cast_pow m n]

Canonical Homomorphism Preserves Powers: $\text{cast}(m^n) = (\text{cast}(m))^n$

Informal description

For any additive monoid with one $\alpha$ and any natural numbers $m$ and $n$, the canonical homomorphism from $\mathbb{N}$ to $\alpha$ satisfies $\text{cast}(m^n) = (\text{cast}(m))^n$.

Nat.cast_dvd_cast theorem

(h : m ∣ n) : (m : α) ∣ (n : α)

Full source

lemma cast_dvd_cast (h : m ∣ n) : (m : α) ∣ (n : α) := map_dvd (Nat.castRingHom α) h

Divisibility Preservation under Canonical Homomorphism: $m \mid n \Rightarrow (m : \alpha) \mid (n : \alpha)$

Informal description

For any natural numbers $m$ and $n$ such that $m$ divides $n$, and for any additive monoid with one $\alpha$, the canonical homomorphism from $\mathbb{N}$ to $\alpha$ preserves divisibility, i.e., $(m : \alpha)$ divides $(n : \alpha)$.

map_natCast' theorem

{A} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B] (f : F) (h : f 1 = 1) : ∀ n : ℕ, f n = n

Full source

theorem map_natCast' {A} [AddMonoidWithOne A] [FunLike F A B] [AddMonoidHomClass F A B]
    (f : F) (h : f 1 = 1) :
    ∀ n : ℕ, f n = n :=
  eq_natCast' ((f : A →+ B).comp <| Nat.castAddMonoidHom _) (by simpa)

Preservation of Natural Number Casting under Additive Monoid Homomorphisms

Informal description

Let $A$ be an additive monoid with one, and let $F$ be a type of functions from $A$ to $B$ that preserves the additive monoid structure. For any function $f \in F$ such that $f(1) = 1$, and for any natural number $n$, we have $f(n) = n$.

map_ofNat' theorem

 {A} [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

Full source

theorem map_ofNat' {A} [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 :=
  map_natCast' f h n

Preservation of Numerals ≥ 2 under Additive Monoid Homomorphisms

Informal description

Let $A$ be an additive monoid with one, and let $F$ be a type of functions from $A$ to $B$ that preserves the additive monoid structure. For any function $f \in F$ such that $f(1) = 1$, and for any natural number $n \geq 2$, we have $f(n) = n$.

ext_nat'' theorem

[ZeroHomClass F ℕ A] (f g : F) (h_pos : ∀ {n : ℕ}, 0 < n → f n = g n) : f = g

Full source

/-- If two `MonoidWithZeroHom`s agree on the positive naturals they are equal. -/
theorem ext_nat'' [ZeroHomClass F ℕ A] (f g : F) (h_pos : ∀ {n : ℕ}, 0 < n → f n = g n) :
    f = g := by
  apply DFunLike.ext
  rintro (_ | n)
  · simp
  · exact h_pos n.succ_pos

Extensionality of Zero-Preserving Functions on Positive Natural Numbers

Informal description

Let $A$ be a type with a zero element, and let $F$ be a type of functions from $\mathbb{N}$ to $A$ that preserves zero. For any two functions $f, g \in F$, if $f(n) = g(n)$ for all positive natural numbers $n$, then $f = g$.

MonoidWithZeroHom.ext_nat theorem

{f g : ℕ →*₀ A} : (∀ {n : ℕ}, 0 < n → f n = g n) → f = g

Full source

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

Extensionality of Monoid Homomorphisms with Zero on Positive Natural Numbers

Informal description

Let $A$ be a type, and let $f, g : \mathbb{N} \to A$ be monoid homomorphisms with zero. If $f(n) = g(n)$ for all positive natural numbers $n$, then $f = g$.

map_natCast theorem

[FunLike F R S] [RingHomClass F R S] (f : F) : ∀ n : ℕ, f (n : R) = n

Full source

@[simp]
theorem map_natCast [FunLike F R S] [RingHomClass F R S] (f : F) : ∀ n : ℕ, f (n : R) = n :=
  map_natCast' f <| map_one f

Preservation of Natural Number Casting under Ring Homomorphisms

Informal description

Let $R$ and $S$ be semirings, and let $F$ be a type of ring homomorphisms from $R$ to $S$. For any ring homomorphism $f \colon R \to S$ and any natural number $n$, the image of the canonical embedding of $n$ in $R$ under $f$ equals $n$ itself, i.e., $f(n) = n$.

map_ofNat theorem

[FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ) [Nat.AtLeastTwo n] : (f ofNat(n) : S) = OfNat.ofNat n

Full source

/-- 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 map_ofNat [FunLike F R S] [RingHomClass F R S] (f : F) (n : ℕ) [Nat.AtLeastTwo n] :
    (f ofNat(n) : S) = OfNat.ofNat n :=
  map_natCast f n

Preservation of Numerals ≥ 2 under Ring Homomorphisms

Informal description

Let $R$ and $S$ be semirings, and let $F$ be a type of ring homomorphisms from $R$ to $S$. For any ring homomorphism $f \colon R \to S$ and any natural number $n \geq 2$, the image of the canonical embedding of $n$ in $R$ under $f$ equals the canonical embedding of $n$ in $S$, i.e., $f(n) = n$.

ext_nat theorem

[FunLike F ℕ R] [RingHomClass F ℕ R] (f g : F) : f = g

Full source

theorem ext_nat [FunLike F ℕ R] [RingHomClass F ℕ R] (f g : F) : f = g :=
  ext_nat' f g <| by simp

Extensionality of Ring Homomorphisms from Natural Numbers

Informal description

For any two ring homomorphisms $f, g \colon \mathbb{N} \to R$ from the natural numbers to a semiring $R$, if $f$ and $g$ agree on all natural numbers, then $f = g$.

NeZero.nat_of_neZero theorem

 {R S} [NonAssocSemiring R] [NonAssocSemiring S] {F} [FunLike F R S] [RingHomClass F R S] (f : F) {n : ℕ}
  [hn : NeZero (n : S)] : NeZero (n : R)

Full source

theorem NeZero.nat_of_neZero {R S} [NonAssocSemiring R] [NonAssocSemiring S]
    {F} [FunLike F R S] [RingHomClass F R S] (f : F)
    {n : ℕ} [hn : NeZero (n : S)] : NeZero (n : R) :=
  .of_map (f := f) (neZero := by simp only [map_natCast, hn])

Non-Zero Preservation of Natural Numbers under Ring Homomorphisms

Informal description

Let $R$ and $S$ be non-associative semirings, and let $F$ be a type of ring homomorphisms from $R$ to $S$. Given a ring homomorphism $f \colon R \to S$ and a natural number $n$, if $n$ is non-zero in $S$ (i.e., $n \neq 0$ in $S$), then $n$ is also non-zero in $R$ (i.e., $n \neq 0$ in $R$).

Nat.cast_id theorem

(n : ℕ) : n.cast = n

Full source

@[simp, norm_cast]
theorem Nat.cast_id (n : ℕ) : n.cast = n :=
  rfl

Identity of Natural Number Casting

Informal description

For any natural number $n$, the canonical embedding of $n$ into a type with a `Nat.cast` operation is equal to $n$ itself, i.e., $\text{cast}(n) = n$.

Nat.castRingHom_nat theorem

: Nat.castRingHom ℕ = RingHom.id ℕ

Full source

@[simp]
theorem Nat.castRingHom_nat : Nat.castRingHom ℕ = RingHom.id ℕ :=
  rfl

Identity of Natural Number Ring Homomorphism to Itself

Informal description

The canonical ring homomorphism from the natural numbers to themselves is equal to the identity ring homomorphism, i.e., $\text{Nat.castRingHom}_{\mathbb{N}} = \text{id}_{\mathbb{N}}$.

Nat.uniqueRingHom instance

{R : Type*} [NonAssocSemiring R] : Unique (ℕ →+* R)

Full source

/-- We don't use `RingHomClass` here, since that might cause type-class slowdown for
`Subsingleton`. -/
instance Nat.uniqueRingHom {R : Type*} [NonAssocSemiring R] : Unique (ℕℕ →+* R) where
  default := Nat.castRingHom R
  uniq := RingHom.eq_natCast'

Uniqueness of the Natural Number Ring Homomorphism to a Non-Associative Semiring

Informal description

For any non-associative semiring $R$, there is exactly one ring homomorphism from the natural numbers $\mathbb{N}$ to $R$.

Pi.instNatCast instance

: NatCast (∀ a, π a)

Full source

instance instNatCast : NatCast (∀ a, π a) where natCast n _ := n

Natural Number Cast on Product Types

Informal description

For any family of types $\pi_a$ indexed by $a \in \alpha$, the type $\prod_{a \in \alpha} \pi_a$ has a natural structure of a type with a canonical map from the natural numbers, where each natural number $n$ is mapped to the constant function with value $n$.

Pi.natCast_apply theorem

(n : ℕ) (a : α) : (n : ∀ a, π a) a = n

Full source

@[simp]
theorem natCast_apply (n : ℕ) (a : α) : (n : ∀ a, π a) a = n :=
  rfl

Evaluation of Constant Function in Product Type

Informal description

For any natural number $n$ and any index $a \in \alpha$, the evaluation of the constant function $n$ (viewed as an element of the product type $\prod_{a \in \alpha} \pi_a$) at $a$ equals $n$, i.e., $(n)_a = n$.

Pi.natCast_def theorem

(n : ℕ) : (n : ∀ a, π a) = fun _ ↦ ↑n

Full source

theorem natCast_def (n : ℕ) : (n : ∀ a, π a) = fun _ ↦ ↑n :=
  rfl

Definition of Natural Number Cast in Product Types

Informal description

For any natural number $n$ and any family of types $\pi_a$ indexed by $a \in \alpha$, the canonical map from $\mathbb{N}$ to the product type $\prod_{a \in \alpha} \pi_a$ sends $n$ to the constant function that maps every $a \in \alpha$ to $n$.

Pi.instOfNat instance

(n : ℕ) [∀ i, OfNat (π i) n] : OfNat ((i : α) → π i) n

Full source

instance (priority := low) instOfNat (n : ℕ) [∀ i, OfNat (π i) n] : OfNat ((i : α) → π i) n where
  ofNat _ := OfNat.ofNat n

Canonical Element in Function Space from Natural Numbers

Informal description

For any natural number $n$ and any family of types $\pi_i$ indexed by $\alpha$ where each $\pi_i$ has a canonical element corresponding to $n$, the function space $\forall (i : \alpha), \pi_i$ also has a canonical element corresponding to $n$.

Pi.ofNat_apply theorem

(n : ℕ) [∀ i, OfNat (π i) n] (a : α) : (ofNat(n) : ∀ a, π a) a = ofNat(n)

Full source

@[simp]
theorem ofNat_apply (n : ℕ) [∀ i, OfNat (π i) n] (a : α) : (ofNat(n) : ∀ a, π a) a = ofNat(n) := rfl

Evaluation of Canonical Function at Index Equals Canonical Element

Informal description

For any natural number $n$ and any family of types $\pi_i$ indexed by $\alpha$ where each $\pi_i$ has a canonical element corresponding to $n$, the evaluation of the canonical function $(n : \forall a, \pi a)$ at any index $a \in \alpha$ equals the canonical element $n$ in $\pi_a$.

Pi.ofNat_def theorem

(n : ℕ) [∀ i, OfNat (π i) n] : (ofNat(n) : ∀ a, π a) = fun _ ↦ ofNat(n)

Full source

lemma ofNat_def (n : ℕ) [∀ i, OfNat (π i) n] : (ofNat(n) : ∀ a, π a) = fun _ ↦ ofNat(n) := rfl

Canonical Element in Function Space as Constant Function

Informal description

For any natural number $n$ and any family of types $\pi_i$ indexed by $\alpha$ where each $\pi_i$ has a canonical element corresponding to $n$, the canonical element in the function space $\forall (i : \alpha), \pi_i$ is the constant function that maps every index to the canonical element of $n$ in the respective type $\pi_i$. That is, $\text{ofNat}(n) = \lambda \_, \text{ofNat}(n)$.

Sum.elim_natCast_natCast theorem

{α β γ : Type*} [NatCast γ] (n : ℕ) : Sum.elim (n : α → γ) (n : β → γ) = n

Full source

theorem Sum.elim_natCast_natCast {α β γ : Type*} [NatCast γ] (n : ℕ) :
    Sum.elim (n : α → γ) (n : β → γ) = n :=
  Sum.elim_lam_const_lam_const (γ := γ) n

Sum Elimination Preserves Natural Number Casts

Informal description

For any types $\alpha$, $\beta$, and $\gamma$ with a canonical map from natural numbers to $\gamma$, and for any natural number $n$, the function obtained by combining the constant functions $n : \alpha \to \gamma$ and $n : \beta \to \gamma$ via the sum elimination operator is equal to the constant function $n : \alpha \oplus \beta \to \gamma$.

Main declarations