OfNat.ofNat_ne_zero
theorem OfNat.ofNat_ne_zero :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo],
OfNat.ofNat n ≠ 0
This theorem states that for any type `R` that is equipped with the structure of an additive monoid with a distinguished one element and has the property of "characteristic zero" (i.e., no natural number other than zero, when considered as an element of `R`, equals the zero element of `R`), and for any natural number `n` that is at least two, the natural number `n` as an element of `R` (obtained through the `OfNat.ofNat` function) is not equal to the zero element of `R`.
More concisely: For any additive monoid `R` with unit and characteristic zero, the natural number `n` (as an element of `R`) is distinct from the zero element for any `n` greater than or equal to 2.
|
Nat.cast_ne_zero
theorem Nat.cast_ne_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
This theorem states that for any natural number 'n' and any type 'R' that is an additive monoid with identity element and has the property of being characteristic zero, the casted value of 'n' to 'R' is not equal to zero if and only if 'n' is not equal to zero. In other words, the natural number 'n' is non-zero if and only if its casted value in the additive monoid 'R' is also non-zero. The characteristic zero property ensures that the additive identity (zero) and multiplicative identity (one) in 'R' correspond with the numbers 0 and 1 in the natural numbers.
More concisely: For any additive monoid with identity element and characteristic zero 'R' and natural number 'n', the cast of 'n' to 'R' is non-zero if and only if 'n' is non-zero.
|
CharZero.cast_injective
theorem CharZero.cast_injective :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [self : CharZero R], Function.Injective Nat.cast
The theorem `CharZero.cast_injective` states that for any type `R` which has an instance of `AddMonoidWithOne` and `CharZero`, the canonical map from natural numbers (`ℕ`) to `R` (denoted as `Nat.cast`) is injective. In mathematical terms, this means if we have a type `R` that is an additive monoid with a distinguished "one" element and has characteristic zero, then for any two natural numbers, if their images in `R` under the canonical map are equal, then the two natural numbers were equal. This injectivity property essentially means no two different natural numbers map to the same element of `R`.
More concisely: If `R` is an additive monoid with a one element and characteristic zero, then the canonical map from natural numbers to `R` is an injection.
|
Mathlib.Algebra.CharZero.Defs._auxLemma.10
theorem Mathlib.Algebra.CharZero.Defs._auxLemma.10 :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo],
(1 = OfNat.ofNat n) = False
The theorem `Mathlib.Algebra.CharZero.Defs._auxLemma.10` states that for any type `R` which is an `AddMonoidWithOne` (an additive monoid with an additional multiplicative identity) and a `CharZero` (a type of algebraic structures where the characteristic is zero), and for any natural number `n` that is at least two, the equality `1 = OfNat.ofNat n` is always false. This means that the numeric literal `1` of type `R` is never equal to the result of applying the `OfNat.ofNat` function to `n`, assuming that `n` is at least two.
More concisely: For any AddMonoidWithOne type R with CharZero structure, the numeric literal 1 is never equal to OfNat.ofNat n for any natural number n ≥ 2.
|
Mathlib.Algebra.CharZero.Defs._auxLemma.7
theorem Mathlib.Algebra.CharZero.Defs._auxLemma.7 :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo],
(OfNat.ofNat n = 0) = False
This theorem, named `Mathlib.Algebra.CharZero.Defs._auxLemma.7`, states for any type `R`, provided that `R` is a type that has an additive monoid with one structure, and a characteristic zero structure. For a natural number `n` that is at least two (`n` is greater than or equal to 2), the proposition that the `OfNat.ofNat` function, which converts this natural number `n` to type `R`, equals zero is always false. In other words, for all such `n` and `R`, `OfNat.ofNat n` cannot be zero.
More concisely: For any type `R` with an additive monoid and characteristic zero structure, the conversion of a natural number `n` (greater than or equal to 2) to `R` is never equal to zero.
|
Nat.cast_injective
theorem Nat.cast_injective :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], Function.Injective Nat.cast
The theorem `Nat.cast_injective` states that for any type `R`, given that `R` is an `AddMonoidWithOne` and has a `CharZero` structure, the function that casts a natural number to `R` is injective. In other words, if two natural numbers are equal after being cast to `R`, then they were originally the same natural number. This theorem asserts that casting doesn't cause any ambiguity or loss of information in the context of natural numbers and the type `R` with the given structures.
More concisely: For types `R` endowed with an `AddMonoidWithOne` and `CharZero` structure, the function that casts natural numbers to `R` is an injection.
|
Nat.cast_inj
theorem Nat.cast_inj : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {m n : ℕ}, ↑m = ↑n ↔ m = n
This theorem, `Nat.cast_inj`, states that for any type `R` that has both an addition operation with an identity element (a `AddMonoidWithOne`) and a characteristic of zero (`CharZero`), the equality of the casted natural numbers `m` and `n` into `R` implies the equality of `m` and `n` themselves, and vice versa. In other words, if two natural numbers `m` and `n` are equal after being cast to type `R`, then `m` and `n` were already equal in the natural numbers, and if `m` and `n` are equal in the natural numbers, they will remain equal after being cast to type `R`.
More concisely: If `R` is a type with an additive monoid structure and characteristic zero, then the casted natural numbers `m` and `n` are equal if and only if the original natural numbers `m` and `n` are equal.
|
Mathlib.Algebra.CharZero.Defs._auxLemma.2
theorem Mathlib.Algebra.CharZero.Defs._auxLemma.2 :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {m n : ℕ}, (↑m = ↑n) = (m = n)
This theorem, `Mathlib.Algebra.CharZero.Defs._auxLemma.2`, states that for any type `R` that is an additive monoid with one and has characteristic zero (these are the `inst` and `inst_1` conditions), and for any natural numbers `m` and `n`, the condition that `m` and `n` are equal when coerced (or, more technically, mapped) to `R` is equivalent to `m` and `n` being equal as natural numbers. In other words, in a characteristic zero additive monoid with one, the natural number coercion function preserves equality.
More concisely: In a commutative additive monoid with one and characteristic zero, the natural number coercion function preserves equality.
|
Mathlib.Algebra.CharZero.Defs._auxLemma.8
theorem Mathlib.Algebra.CharZero.Defs._auxLemma.8 :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo],
(0 = OfNat.ofNat n) = False
This theorem, named `Mathlib.Algebra.CharZero.Defs._auxLemma.8`, states that for any type `R` which represents a mathematical structure exhibiting characteristics of an additive monoid with one and character zero, and for any natural number `n` that is at least two, the assertion that zero is equal to the natural number `n` when `n` is interpreted as an element of type `R` via the `OfNat.ofNat` function, is always false. This theorem is essentially saying that no natural number `n` that is at least two can be equivalent to zero in a character zero algebraic structure.
More concisely: In any additive monoid with a character zero element, zero is not equal to any natural number greater than one.
|
Mathlib.Algebra.CharZero.Defs._auxLemma.3
theorem Mathlib.Algebra.CharZero.Defs._auxLemma.3 :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : ℕ}, (↑n = 0) = (n = 0)
This theorem, `Mathlib.Algebra.CharZero.Defs._auxLemma.3`, states that for any given type `R`, if `R` is an additive monoid with an identity element (one) and `R` is characteristic zero, then for any natural number `n`, the statement that the characteristic of `n` being equal to zero is equivalent to `n` itself being zero. In other words, in such a type `R`, a natural number `n` has a characteristic of zero if and only if `n` equals zero. The characteristic of an element in a ring is the smallest positive integer such that the element times this integer equals zero, or it's zero if no such integer exists.
More concisely: In an additive monoid with identity and characteristic zero, the characteristic of a natural number equals zero if and only if the number is zero.
|
Nat.cast_eq_zero
theorem Nat.cast_eq_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : ℕ}, ↑n = 0 ↔ n = 0
This theorem states that for any type `R` that has structures of `AddMonoidWithOne` and `CharZero`, a natural number `n` cast to type `R` is equal to zero if and only if `n` is equal to zero. Here, `AddMonoidWithOne` implies that `R` has operations of addition and multiplication with an identity element, and `CharZero` means that distinct natural numbers map to distinct elements of `R`. The theorem ensures that the zero element in the natural numbers and in `R` correspond under this mapping.
More concisely: For any type `R` with `AddMonoidWithOne` and `CharZero` structures, the natural number `0` maps to the additive identity `0` in `R`.
|
Mathlib.Algebra.CharZero.Defs._auxLemma.9
theorem Mathlib.Algebra.CharZero.Defs._auxLemma.9 :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] (n : ℕ) [inst_2 : n.AtLeastTwo],
(OfNat.ofNat n = 1) = False
This theorem, named `Mathlib.Algebra.CharZero.Defs._auxLemma.9`, states that for any type `R` which is both an additive monoid with one (i.e., a structure with an associative addition operation and a multiplicative operation where the multiplication is associative, has an identity, and distributes over addition) and has characteristic zero (`CharZero R` implies that each natural number maps to a distinct element of `R`), and for any natural number `n` satisfying the property `Nat.AtLeastTwo n` (i.e., `n` is at least 2), the assertion that `OfNat.ofNat n` (the interpretation of the natural number `n` as an element of the type `R`) equals 1 is always false. In other words, any natural number that is at least two cannot be interpreted as 1 in any additive monoid with one of characteristic zero.
More concisely: In an additive monoid with one of characteristic zero, no natural number greater than one can be equal to the identity element.
|