zsmul_eq_mul
theorem zsmul_eq_mul : ∀ {α : Type u_3} [inst : Ring α] (a : α) (n : ℤ), n • a = ↑n * a
This theorem states that for every type `α` that forms a ring and for every element `a` of type `α` and integer `n`, the operation of "scalar multiplication" (`n • a`) is equivalent to converting `n` into the ring type and then performing ring multiplication (`↑n * a`). Essentially, it says that scalar multiplication by an integer in a ring is the same as ring multiplication.
More concisely: For every ring `α` and integer `n`, scalar multiplication `n • a` equals ring multiplication `↑n * a` for all `a` in `α`.
|
Mathlib.Data.Int.Cast.Lemmas._auxLemma.8
theorem Mathlib.Data.Int.Cast.Lemmas._auxLemma.8 :
∀ {α : Type u_3} [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, (↑m < ↑n) = (m < n)
This theorem, from the Mathlib library in Lean, states that for any ordered ring `α` that is nontrivial (i.e., it contains at least two distinct elements), the inequality relation between two integers `m` and `n` remains unchanged when they are cast to elements of the ordered ring `α`. More specifically, if `m` is less than `n` in the integers, then the cast of `m` to `α` is less than the cast of `n` to `α`, and vice versa.
More concisely: For any nontrivial ordered ring `α`, if `m < n` in the integers, then `α(m) < α(n)`.
|
Int.coe_nat_pow
theorem Int.coe_nat_pow : ∀ (m n : ℕ), ↑(m ^ n) = ↑m ^ n
This theorem states that for any two natural numbers `m` and `n`, the operation of raising m to the power of n, then coercing the result to an integer, is the same as first coercing m to an integer and then raising it to the power of n. In mathematical terms, it says that for all natural numbers `m` and `n`, `(m^n)` coerced to an integer equals `(m coerced to an integer)^n`.
More concisely: For all natural numbers m and n, (m^n) converted to an integer equals (m converted to an integer)^n.
|
Int.cast_lt
theorem Int.cast_lt : ∀ {α : Type u_3} [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, ↑m < ↑n ↔ m < n := by
sorry
This theorem states that for any given ordered ring `α` and for any two integers `m` and `n`, the casting of `m` to `α` is less than the casting of `n` to `α` if and only if `m` is less than `n`. This theorem essentially establishes that the inequality relationship between two integers is preserved when they are cast into an ordered ring.
More concisely: For any ordered ring `α` and integers `m` and `n`, `m < n` if and only if `cast_int α m < cast_int α n`.
|
eq_intCast
theorem eq_intCast :
∀ {F : Type u_1} {α : Type u_3} [inst : NonAssocRing α] [inst_1 : FunLike F ℤ α] [inst_2 : RingHomClass F ℤ α]
(f : F) (n : ℤ), f n = ↑n
The theorem `eq_intCast` states that for any type `F` and `α`, where `α` is a non-associative ring, `F` is a type which behaves like a function from integers to `α` (expressed by the `FunLike F ℤ α` instance), and `F` is a ring homomorphism from integers to `α` (expressed by the `RingHomClass F ℤ α` instance), then for any function `f` of type `F` and any integer `n`, the result of applying `f` to `n` is equal to the integer value of `n` coerced to type `α` (expressed by `f n = ↑n`).
More concisely: For any non-associative ring `α` and a ring homomorphism `F : ℤ → α` (behaving like a function), `F(n) = ↑n` for all integers `n`.
|
Int.cast_le
theorem Int.cast_le : ∀ {α : Type u_3} [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, ↑m ≤ ↑n ↔ m ≤ n := by
sorry
This theorem, `Int.cast_le`, states that for any type `α` that is an ordered ring and nontrivial, the inequality between two integers `m` and `n` holds true if and only if the same inequality holds true when these integers are cast to the type `α`. In other words, casting does not change the order of the integers.
More concisely: For any nontrivial ordered ring type `α`, the relation `m < n` holds if and only if the relation between the integer casts `α m` and `α n` also holds.
|
Int.cast_nonneg
theorem Int.cast_nonneg : ∀ {α : Type u_3} [inst : OrderedRing α] [inst_1 : Nontrivial α] {n : ℤ}, 0 ≤ ↑n ↔ 0 ≤ n := by
sorry
The theorem `Int.cast_nonneg` states that for any integer `n` and for any ordered ring `α` that is nontrivial (meaning it has at least two distinct elements), the integer `n` is non-negative if and only if the corresponding element in the ring `α` (obtained by casting `n`) is also non-negative. In mathematical terms, this can be expressed as: for any integer `n` and any ordered ring `α`, `0 ≤ n` if and only if `0 ≤ ↑n` in `α`.
More concisely: For any integer `n` and ordered ring `α`, `0 ≤ n` if and only if `0 ≤ α.cast n`.
|
zsmul_one
theorem zsmul_one : ∀ {α : Type u_3} [inst : AddGroupWithOne α] (n : ℤ), n • 1 = ↑n
This theorem, named `zsmul_one`, states that for any integer `n` and for any type `α` that is a AddGroupWithOne (an additive group with a distinguished element 1), the scalar multiplication of `n` and 1 is equal to the coersion of `n` to `α`. In other words, multiplying 1 by any integer in an additive group with one is equal to the integer itself (after proper type coersion).
More concisely: For any integer `n` and additive group with one `α`, the operation of scaling `n` by 1 in `α` is equal to the coercion of `n` to `α`.
|
AddMonoidHom.ext_int
theorem AddMonoidHom.ext_int : ∀ {A : Type u_5} [inst : AddMonoid A] {f g : ℤ →+ A}, f 1 = g 1 → f = g
This theorem states that for any type `A` that has an additive monoid structure, if `f` and `g` are two additive monoid homomorphisms from the integers to `A`, and if `f` and `g` map the integer `1` to the same element in `A`, then `f` and `g` are indeed the same homomorphism. In other words, for additive monoid homomorphisms from the integers to any additive monoid, the value of the homomorphism at `1` completely determines the homomorphism.
More concisely: If `A` is an additive monoid and `f` and `g` are homomorphisms from the integers to `A` with `f(1) = g(1)`, then `f = g`.
|
map_intCast
theorem map_intCast :
∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : NonAssocRing α] [inst_1 : NonAssocRing β]
[inst_2 : FunLike F α β] [inst_3 : RingHomClass F α β] (f : F) (n : ℤ), f ↑n = ↑n
The theorem `map_intCast` states that for any types `F`, `α` and `β`, where `α` and `β` are non-associative rings, `F` is a function-like object from `α` to `β`, and `F` is a ring homomorphism from `α` to `β`, the function `f` of type `F` preserves the cast of an integer `n` to `α` and `β`. In other words, applying `f` to the cast of `n` to `α` is the same as the cast of `n` to `β`. This theorem expresses an important property of ring homomorphisms: they preserve the ring structure, in this case, the ability to cast integers to members of the ring.
More concisely: For any ring homomorphism `F` from non-associative rings `α` and `β`, and any integer `n`, `F (int.cast α n) = int.cast β (n)`.
|
Int.cast_commute
theorem Int.cast_commute : ∀ {α : Type u_3} [inst : NonAssocRing α] (n : ℤ) (a : α), Commute (↑n) a
This theorem, `Int.cast_commute`, states that for any type `α` that has a `NonAssocRing` structure, an integer `n`, and an element `a` of type `α`, the result of integer `n` cast to type `α` commutes with element `a`. In other words, for any integer `n` and element `a` of a non-associative ring, the product of `n` and `a` is equal to the product of `a` and `n`. This is expressed in mathematical notation as `n * a = a * n`.
More concisely: For any non-associative ring type `α` and integer `n`, the operation of multiplying `n` with an element `a` in `α` is commutative, i.e., `n * a = a * n`.
|
Mathlib.Data.Int.Cast.Lemmas._auxLemma.7
theorem Mathlib.Data.Int.Cast.Lemmas._auxLemma.7 :
∀ {α : Type u_3} [inst : OrderedRing α] [inst_1 : Nontrivial α] {m n : ℤ}, (↑m ≤ ↑n) = (m ≤ n)
This theorem, named `Mathlib.Data.Int.Cast.Lemmas._auxLemma.7`, states that for any type `α` which is part of an ordered ring and is nontrivial, and for any two integers `m` and `n`, the inequality `m` less than or equal to `n` holds if and only if the cast of `m` to type `α` is less than or equal to the cast of `n` to type `α`. In other words, the ordering of `m` and `n` remains the same when they are cast to another type in an ordered ring.
More concisely: For any nontrivial ordered ring type `α`, if `m` ≤ `n` holds in the integers, then the casts `α(m)` and `α(n)` satisfy `α(m) ≤ α(n)`.
|
ext_int'
theorem ext_int' :
∀ {F : Type u_1} {α : Type u_3} [inst : MonoidWithZero α] [inst_1 : FunLike F ℤ α]
[inst : MonoidWithZeroHomClass F ℤ α] {f g : F}, f (-1) = g (-1) → (∀ (n : ℕ), 0 < n → f ↑n = g ↑n) → f = g
This theorem states that for any type `F` and `α`, given the conditions that `α` is a `MonoidWithZero` and `F` behaves like a function from integers to `α` (`FunLike F ℤ α`), and that `F` is a `MonoidWithZeroHomClass`, if two instances of this function `f` and `g` agree on `-1` and on all positive natural numbers, then `f` and `g` are indeed the same function. In more mathematical terms, given two `MonoidWithZeroHom`s `f` and `g`, if `f(-1) = g(-1)` and `f(n) = g(n)` for all positive natural numbers `n`, then `f` is equal to `g`.
More concisely: If `F` is a `MonoidWithZeroHomClass` function from integers to a `MonoidWithZero` type `α`, such that `f` and `g` are two instances of this function with `f(-1) = g(-1)` and `f(n) = g(n)` for all positive natural numbers `n`, then `f` is equal to `g`.
|
Int.cast_abs
theorem Int.cast_abs : ∀ {α : Type u_3} [inst : LinearOrderedRing α] {a : ℤ}, ↑|a| = |↑a|
This theorem, `Int.cast_abs`, states that for any integer `a` and any type `α` that is a linear ordered ring, the absolute value of the casted integer `a` to type `α` is the same as the cast of the absolute value of `a` to type `α`. In other words, the operations of taking the absolute value and casting an integer to another type commute with each other.
More concisely: For any integer `a` and linear ordered ring `α`, |α(a)| = α( $|$a$|$ ).
|
MonoidHom.ext_int
theorem MonoidHom.ext_int :
∀ {M : Type u_5} [inst : Monoid M] {f g : ℤ →* M},
f (-1) = g (-1) → f.comp ↑Int.ofNatHom = g.comp ↑Int.ofNatHom → f = g
This theorem states that for any type `M` that is a monoid, if we have two monoid homomorphisms `f` and `g` from the integers (`ℤ`) to `M`, then if `f` and `g` agree on the value `-1` and on all natural numbers (which are implicitly included in the integers via the `Int.ofNatHom` coercion), then `f` and `g` must be the same homomorphism. This is a kind of uniqueness result for monoid homomorphisms from integers to any given monoid, under certain conditions.
More concisely: If `M` is a monoid and `f` and `g` are homomorphisms from `ℤ` to `M` such that `f(-1) = g(-1)` and `f(n) = g(n)` for all natural numbers `n`, then `f = g`.
|
Int.commute_cast
theorem Int.commute_cast : ∀ {α : Type u_3} [inst : NonAssocRing α] (a : α) (n : ℤ), Commute a ↑n
The theorem `Int.commute_cast` states that for any given type α, which is a Non-Associative Ring, and any elements `a` from α and `n` from the set of integers, the operation of multiplication of `a` and the cast of `n` to α (denoted as ↑n) commutes. In other words, for any integer `n` and any element `a` in a Non-Associative Ring α, we have `a * ↑n = ↑n * a`.
More concisely: For any non-associative ring α and integers n and a in α, the multiplication of a and the cast of n to α commutes: a * ↑n = ↑n * a.
|
Int.coe_nat_pos
theorem Int.coe_nat_pos : ∀ {n : ℕ}, 0 < ↑n ↔ 0 < n
This theorem states that for any natural number `n`, the statement "zero is less than the integer representation of `n`" is equivalent to "zero is less than `n`". In other words, a natural number `n` is positive if and only if its corresponding integer is positive.
More concisely: For any natural number `n`, the statement "0 < int.of_nat `n`" is equivalent to "0 < `n`".
|
MonoidWithZeroHom.ext_int
theorem MonoidWithZeroHom.ext_int :
∀ {M : Type u_5} [inst : MonoidWithZero M] {f g : ℤ →*₀ M},
f (-1) = g (-1) → f.comp Int.ofNatHom.toMonoidWithZeroHom = g.comp Int.ofNatHom.toMonoidWithZeroHom → f = g
This theorem states that for any type `M` that has a `MonoidWithZero` structure, if there are two monoid homomorphisms `f` and `g` from the integers (`ℤ`) to `M`, and they agree on the values of `-1` and all natural numbers (`ℕ`), then these two homomorphisms must be the same. In other words, any two homomorphisms from the integers to a monoid with zero are uniquely determined by their values on `-1` and the natural numbers.
More concisely: Given any monoid `M` with a `MonoidWithZero` structure and two homomorphisms `f` and `g` from the integers (ℤ) to `M` such that `f(-1) = g(-1)` and `f(n) = g(n)` for all natural numbers `n`, then `f = g`.
|
RingHom.ext_int
theorem RingHom.ext_int : ∀ {R : Type u_5} [inst : NonAssocSemiring R] (f g : ℤ →+* R), f = g
This theorem states that for any type `R` which is an instance of a Non-Associative Semiring, all ring homomorphisms from the integers (`ℤ`) to `R` are equal. That means, given any two ring homomorphisms `f` and `g` from the integers to `R`, `f` and `g` must be the same. The theorem sheds light on the uniqueness property of such ring homomorphisms.
More concisely: For any type `R` being an instance of a Non-Associative Semiring, there exists at most one ring homomorphism from the integers to `R`.
|