ext_nat'
theorem ext_nat' :
∀ {A : Type u_3} {F : Type u_5} [inst : FunLike F ℕ A] [inst_1 : AddMonoid A] [inst_2 : AddMonoidHomClass F ℕ A]
(f g : F), f 1 = g 1 → f = g
The theorem `ext_nat'` states that for any two functions `f` and `g` of type `F`, where `F` is a function-like type that maps natural numbers (`ℕ`) to another type `A`, under the conditions that `A` is an additive monoid and `F` is a class of homomorphisms preserving the additive monoid structure from natural numbers to `A`, if `f` and `g` have the same output when applied to the natural number 1, then `f` and `g` must be the same function. This theorem essentially asserts the uniqueness of such functions based on their values at the point 1.
More concisely: If `F` maps natural numbers to an additive monoid `A` and `f` and `g` are functions of type `F` with `f 1 = g 1`, then `f = g`.
|
map_natCast'
theorem map_natCast' :
∀ {B : Type u_4} {F : Type u_5} [inst : AddMonoidWithOne B] {A : Type u_6} [inst_1 : AddMonoidWithOne A]
[inst_2 : FunLike F A B] [inst_3 : AddMonoidHomClass F A B] (f : F), f 1 = 1 → ∀ (n : ℕ), f ↑n = ↑n
The theorem `map_natCast'` states that for any types `B`, `F`, and `A`, given that `B` and `A` are both AddMonoidWithOne (which means they are both additive monoids with a distinguished element `1`), `F` is a function from type `A` to `B`, and `F` is a homomorphism class for the add monoid, then for any function `f` of type `F`, if `f` maps `1` of `A` to `1` of `B`, then `f` preserves the natural number casting, i.e., for all natural numbers `n`, the result of casting `n` to `A` and then applying `f` is the same as directly casting `n` to `B`.
More concisely: If `F` is a homomorphism from an additive monoid `A` with identity `1` to an additive monoid `B` with identity `1`, and `F(1) = 1`, then for all natural numbers `n`, `F(n : A) = (n : B)`.
|
MonoidHom.ext_mnat
theorem MonoidHom.ext_mnat :
∀ {α : Type u_1} [inst : Monoid α] ⦃f g : Multiplicative ℕ →* α⦄,
f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1) → f = g
This theorem states that for any type `α` that forms a Monoid, two monoid homomorphisms `f` and `g` from `Multiplicative ℕ` to `α` are equal if they map the element `1` (reinterpreted multiplicatively) to the same value. In other words, the identity of the monoid homomorphisms is determined by their value at `1` in the natural numbers under the multiplicative interpretation.
More concisely: If `f` and `g` are monoid homomorphisms from the multiplicative monoid of natural numbers to a monoid `α`, then `f = g` if and only if `f 1 = g 1`.
|
nsmul_eq_mul'
theorem nsmul_eq_mul' : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (a : α) (n : ℕ), n • a = a * ↑n
This theorem states that for any type `α` that forms a non-associative semiring and for any element `a` of type `α` and `n` of type `ℕ` (natural number), the `n`-fold repetition of the operation on `a` (denoted by `n • a`) is equal to the product of `a` and the natural number `n` (denoted by `a * ↑n`). Here, `↑n` denotes the coercion of natural number `n` into type `α`. This theorem basically connects the concept of repeated addition (n-fold operation) with multiplication in a non-associative semiring.
More concisely: For any non-associative semiring type `α` and its element `a` of type `α` and natural number `n`, the `n`-fold repetition of the operation on `a`, `n • a`, is equivalent to the product of `a` and the natural number `n`, `a * ↑n`.
|
ext_nat''
theorem ext_nat'' :
∀ {A : Type u_3} {F : Type u_4} [inst : MulZeroOneClass A] [inst_1 : FunLike F ℕ A]
[inst : MonoidWithZeroHomClass F ℕ A] (f g : F), (∀ {n : ℕ}, 0 < n → f n = g n) → f = g
The theorem `ext_nat''` states that for any type `A` equipped with a multiplication, zero, and one (`MulZeroOneClass A`), and any type `F` that can be seen as a function from natural numbers to `A` (`FunLike F ℕ A`), if `F` is a multiplicative monoid homomorphism with zero (`MonoidWithZeroHomClass F ℕ A`), then any two elements `f` and `g` of `F` are equal if they agree on all positive natural numbers. In other words, if for every positive natural number `n`, `f(n)` equals `g(n)`, then `f` and `g` are the same homomorphism.
More concisely: If `F` is a multiplicative monoid homomorphism from the natural numbers to a type `A` equipped with multiplication, zero, and one, then `F` is determined by its values on positive natural numbers.
|
nsmul_one
theorem nsmul_one : ∀ {A : Type u_6} [inst : AddMonoidWithOne A] (n : ℕ), n • 1 = ↑n
This theorem states that for any natural number `n` and for any type `A` that is an additive monoid with a distinguished one element, the operation of scaling the one element by `n` (denoted by `n • 1`) is equal to the natural number `n` itself when viewed as an element of the monoid `A` (denoted by `↑n`). In other words, if you add one to itself `n` times in the additive monoid `A`, you get `n`.
More concisely: For any additive monoid with identity element `A` and natural number `n`, the operation of scaling the identity `n` times equals `n` itself in `A`.
|
AddMonoidHom.ext_nat
theorem AddMonoidHom.ext_nat : ∀ {A : Type u_3} [inst : AddMonoid A] {f g : ℕ →+ A}, f 1 = g 1 → f = g
This theorem states that for any given type `A` that is an additive monoid, and any two additive monoid homomorphisms `f` and `g` from natural numbers to `A`, if `f` and `g` are the same on input `1`, then `f` and `g` are identical functions. This is a statement of the uniqueness of the monoid homomorphisms in this specific setting.
More concisely: If `A` is an additive monoid and `f` and `g` are additive monoid homomorphisms from the natural numbers to `A` with `f(1) = g(1)`, then `f = g`.
|
eq_natCast
theorem eq_natCast :
∀ {R : Type u_3} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : FunLike F ℕ R] [inst_2 : RingHomClass F ℕ R]
(f : F) (n : ℕ), f n = ↑n
The theorem `eq_natCast` states that for any type `R` that forms a non-associative semiring, for any type `F` that is function-like from natural numbers to `R` and for any ring homomorphism class from natural numbers to `R`, any function `f : F` when evaluated at a natural number `n` is equal to the cast of `n` to `R`. In other words, this theorem asserts that for these given conditions, the action of the function `f` on natural numbers is equivalent to just casting the natural numbers to the type `R`.
More concisely: For any non-associative semiring type R, any function-like F from natural numbers to R, and any ring homomorphism f : F, the evaluation of f at a natural number n equals the cast of n to R.
|
Mathlib.Data.Nat.Cast.Basic._auxLemma.1
theorem Mathlib.Data.Nat.Cast.Basic._auxLemma.1 :
∀ {α : Type u_1} [inst : NonAssocSemiring α] (m n : ℕ), ↑m * ↑n = ↑(m * n)
This theorem states that for any type `α` that is a `NonAssocSemiring`, and any two natural numbers `m` and `n`, the cast of the product of `m` and `n` to `α` is equal to the product of the casts of `m` and `n` to `α`. In mathematical terms, this translates to the assertion that for any non-associative semiring `α`, multiplication is preserved under the casting from natural numbers to `α`, i.e., `↑m * ↑n = ↑(m * n)`.
More concisely: For any non-associative semiring `α`, the casting of the product of two natural numbers to `α` is equal to the product of the castings of those numbers to `α`. In mathematical notation: `↑(m * n) = ↑m * ↑n`.
|
Nat.cast_mul
theorem Nat.cast_mul : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (m n : ℕ), ↑(m * n) = ↑m * ↑n
This theorem states that for all natural numbers `m` and `n`, and for any type `α` that forms a non-associative semiring, the cast of the product of `m` and `n` to type `α` is equal to the product of the cast of `m` and the cast of `n` to type `α`. In mathematical notation, this could be represented as: if `m` and `n` are natural numbers, and `α` is a non-associative semiring, then `(m * n) = m * n` holds true when all quantities are cast to `α`.
More concisely: For any non-associative semiring type `α` and natural numbers `m` and `n`, the cast of `m * n` to `α` equals `m * n` (where `*` denotes both the natural number multiplication and the semiring multiplication).
|
Nat.cast_id
theorem Nat.cast_id : ∀ (n : ℕ), ↑n = n
This theorem states that for any natural number 'n', the coercion (casting) of 'n' to a natural number is equal to 'n' itself. In other words, if you have a natural number and you convert it to a natural number, you will still have the same number. This is a fundamental property of typecasting within the set of natural numbers in Lean 4.
More concisely: For all natural numbers n, the coercion of n to a natural number is equal to n itself. (or) The coercion from a natural number to itself is the identity function.
|
nsmul_eq_mul
theorem nsmul_eq_mul : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (a : α), n • a = ↑n * a
This theorem states that for all types `α` in a non-associative semiring, the scalar multiplication of a natural number `n` and an element `a` from the semiring is equal to the multiplication of the cast of `n` to the semiring and `a`. More formally, given any natural number `n` and any element `a` of the semiring `α`, `n • a` equals `↑n * a`.
More concisely: For any natural number $n$ and element $a$ in a non-associative semiring $\alpha$, $n \cdot a = \uparrow n \times a$.
|
Dvd.dvd.natCast
theorem Dvd.dvd.natCast : ∀ {α : Type u_1} [inst : Semiring α] {m n : ℕ}, m ∣ n → ↑m ∣ ↑n
This theorem, `Dvd.dvd.natCast`, is an alias of `Nat.cast_dvd_cast`. It states that for any semiring `α`, and for any natural numbers `m` and `n`, if `m` divides `n` then the cast of `m` to `α` divides the cast of `n` to `α`. In other words, the divisibility relationship is preserved when natural numbers are cast to elements of any semiring.
More concisely: For any semiring `α`, if `m` divides `n` in the natural numbers, then the cast of `m` to `α` divides the cast of `n` to `α`.
|
Nat.cast_pow
theorem Nat.cast_pow : ∀ {α : Type u_1} [inst : Semiring α] (m n : ℕ), ↑(m ^ n) = ↑m ^ n
This theorem states that for any natural numbers `m` and `n`, and any semiring `α`, the cast of the power `m^n` to `α` is equal to the power of the cast of `m` to `α` raised to `n`. In mathematical terms, it asserts that `(m^n : α) = (m : α)^n` for all natural numbers `m` and `n` and any semiring `α`. This is a property related to the interplay between exponentiation and type casting in semirings.
More concisely: For any natural numbers m and n and semiring α, the cast of m raised to the power n equals the power of the cast of m in α. In other words, (m^n : α) = (m : α)^n.
|
map_natCast
theorem map_natCast :
∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
[inst_2 : FunLike F R S] [inst_3 : RingHomClass F R S] (f : F) (n : ℕ), f ↑n = ↑n
The theorem `map_natCast` states that for any types `R`, `S` and `F`, where `R` and `S` are non-associative semirings, `F` is a function-like structure from `R` to `S`, and `F` forms a ring homomorphism from `R` to `S`, then for any function `f` of type `F` and any natural number `n`, the result of applying `f` to the cast of `n` into `R` (denoted by `f ↑n`) is equal to the cast of `n` into `S` (denoted by `↑n`). This theorem essentially asserts that the function `f` preserves the natural number under its operation, which is a property usually expected of homomorphisms.
More concisely: For any non-associative semirings R, S, and a ring homomorphism F from R to S, for all natural numbers n, we have F (cast n to R) = cast n to S.
|
Mathlib.Data.Nat.Cast.Basic._auxLemma.2
theorem Mathlib.Data.Nat.Cast.Basic._auxLemma.2 : ∀ {α : Type u_1} [inst : Semiring α] (m n : ℕ), ↑m ^ n = ↑(m ^ n)
This theorem states that for any semiring `α` and natural numbers `m` and `n`, the power of the cast of `m` to `n` in `α` is equal to the cast in `α` of the power of `m` to `n`. In other words, the process of casting doesn't change the outcome of the exponentiation operation. It holds true for all types `α` that have a semiring structure.
More concisely: For any semiring `α` and natural numbers `m` and `n`, the cast of `m` to the power of `n` in `α` equals the power of the cast of `m` in `α`.
|
RingHom.eq_natCast'
theorem RingHom.eq_natCast' : ∀ {R : Type u_3} [inst : NonAssocSemiring R] (f : ℕ →+* R), f = Nat.castRingHom R := by
sorry
This theorem states that for any type `R` which is an instance of a `NonAssocSemiring`, any ring homomorphism `f` from the natural numbers (`ℕ`) to `R` is identical to the standard natural number casting function `Nat.castRingHom R`. In other words, any mapping that preserves the ring structure from natural numbers to a non-associative semiring is equivalent to the canonical way of embedding natural numbers into the semiring.
More concisely: For any non-associative semiring `R` and ring homomorphism `f` from the natural numbers to `R`, `f` is equal to the natural number casting function `Nat.castRingHom R`.
|
map_ofNat
theorem map_ofNat :
∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
[inst_2 : FunLike F R S] [inst_3 : RingHomClass F R S] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo],
f (OfNat.ofNat n) = OfNat.ofNat n
This theorem, `map_ofNat`, states that for any types `R`, `S`, and `F`, if `R` and `S` are both non-associative semirings, `F` has an injective function-like coercion to functions from `R` to `S`, `F` is a ring homomorphism from `R` to `S`, `f` is a term of type `F`, and `n` is a natural number such that `n` is at least two, then applying `f` to the result of the function `OfNat.ofNat` applied to `n` gives the same result as applying `OfNat.ofNat` to `n` directly. Essentially, this means that the homomorphism `f` preserves the behaviour of the `OfNat.ofNat` function for natural numbers greater than or equal to two.
More concisely: For any non-associative semirings R, S, and a ring homomorphism F from R to S with injective function-like coercion, if F(OfNat.ofNat n) = OfNat.ofNat m for some natural numbers n and m with n >= 2, then n = m.
|