AddMonoidWithOne.natCast_zero
theorem AddMonoidWithOne.natCast_zero : ∀ {R : Type u_2} [self : AddMonoidWithOne R], NatCast.natCast 0 = 0
This theorem states that for any type `R` which forms an `AddMonoidWithOne`, the canonical mapping from natural numbers (ℕ) to `R`, specifically the `NatCast.natCast`, sends the natural number `0` to the `0` of type `R`. An `AddMonoidWithOne` is a mathematical structure that has an addition operation, and a distinct element `1` that serves as an identity for multiplicative operations. This means that the zero element of the natural numbers is mapped to the zero element of any such type `R` by this natural number casting function.
More concisely: For any type `R` with an `AddMonoidWithOne` structure, the natural number casting function `NatCast.natCast` maps the natural number `0` to the additive identity (zero) of `R`.
|
two_add_one_eq_three
theorem two_add_one_eq_three : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], 2 + 1 = 3
This theorem states that, for any type `α` that has an associated `AddMonoidWithOne` instance (which means that `α` has both an addition operation and a distinct element identified as 'one'), the value of adding `2` and `1` is `3`. This needs to hold true regardless of what the specific type `α` might be; it could be integers, rational numbers, real numbers, or any other type that supports the required operations.
More concisely: For any type `α` with an `AddMonoidWithOne` structure, `(2 : α) + (1 : α) = 3 : α`.
|
Nat.cast_add_one
theorem Nat.cast_add_one : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ), ↑(n + 1) = ↑n + 1
This theorem states that for any natural number `n`, the cast of `n + 1` to some type `R` that is an additive monoid with one, equals the cast of `n` to `R` plus one. In other words, when a natural number `n` is incremented by 1 and then cast to `R`, it is the same as if `n` was first cast to `R` and then incremented by 1. This property holds for all types `R` that have an addition operation and a distinguished element called "one".
More concisely: For any additive monoid with one `R` and natural number `n`, the cast of `n + 1` to `R` equals the cast of `n` to `R` plus one.
|
AddCommMonoidWithOne.add_comm
theorem AddCommMonoidWithOne.add_comm : ∀ {R : Type u_2} [self : AddCommMonoidWithOne R] (a b : R), a + b = b + a := by
sorry
The theorem `AddCommMonoidWithOne.add_comm` states that for any given type `R` that has a structure of an additive commutative monoid with a distinct one element, the addition operation is commutative. In other words, for any two elements `a` and `b` of type `R`, the result of `a` added to `b` is the same as `b` added to `a`.
More concisely: For any additive commutative monoid with one element `R`, the operation `+` is commutative, i.e., `a + b = b + a` for all elements `a, b` of `R`.
|
Nat.cast_add
theorem Nat.cast_add : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (m n : ℕ), ↑(m + n) = ↑m + ↑n
This theorem states that for any type `R`, which is an additive monoid with one, and for any natural numbers `m` and `n`, the cast of the sum of `m` and `n` to `R` is equal to the sum of the cast of `m` to `R` and the cast of `n` to `R`. In other words, in terms of mathematical notation, given a ring `R` and natural numbers `m` and `n`, we have `(m + n) ∈ R = m ∈ R + n ∈ R`.
More concisely: For any additive monoid with one `R` and natural numbers `m` and `n`, the cast of `m + n` to `R` equals the cast of `m` to `R` plus the cast of `n` to `R`. In mathematical notation: `(m + n: R) = (m: R) + (n: R)`.
|
Nat.cast_zero
theorem Nat.cast_zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], ↑0 = 0
This theorem states that for any type `R` which includes addition (`AddMonoid`) and has a distinguished 'one' element (`WithOne`), casting the natural number zero (`0`) to `R` will always yield the 'zero' element of `R`. In other words, it proves that zero in the natural numbers and zero in `R` are equivalent when treated under these conditions, which is a fundamental assumption in number theory and algebra.
More concisely: For any `AddMonoid` and `WithOne` type `R`, the natural number zero maps to the additive identity (zero) of `R`.
|
Nat.AtLeastTwo.one_lt
theorem Nat.AtLeastTwo.one_lt : ∀ {n : ℕ} [inst : n.AtLeastTwo], 1 < n
This theorem states that for any natural number `n` that is at least two, `n` is greater than one. In other words, if a natural number `n` satisfies the property of being at least two (as enforced by `Nat.AtLeastTwo`), then `n` is always strictly larger than one.
More concisely: For any natural number `n` with `n ≥ 2`, we have `n > 1`.
|
Nat.cast_two
theorem Nat.cast_two : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], ↑2 = 2
This theorem, `Nat.cast_two`, states that for any type `R` that is an instance of the typeclass `AddMonoidWithOne`, the natural number cast of `2` to `R` is equal to `2`. In other words, within the context of an additive monoid with a distinct one element, casting the natural number `2` to any such type `R` will result in `2` of type `R`.
More concisely: For any additive monoid with one unit `R`, the conversion of the natural number `2` to `R` is equal to `2` in `R`.
|
one_add_one_eq_two
theorem one_add_one_eq_two : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], 1 + 1 = 2
This theorem states that in any type `α` that is an additive monoid with a unit (`AddMonoidWithOne`), the sum of `1` and `1` equals `2`. An additive monoid with a unit is a mathematical structure that includes an addition operation and a distinguished element called `1` that serves as an "identity element" for multiplication. Thus, the theorem can be thought of as formalizing the intuitive notion that "one plus one equals two" in this general context.
More concisely: In an additive monoid with a unit, the sum of two units is equal to the monoid's unit element with multiplicity two. (Or, more simply: In an additive monoid with a unit, 1 + 1 = 2.)
|
Nat.cast_bit0
theorem Nat.cast_bit0 : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ), ↑(bit0 n) = bit0 ↑n
The theorem `Nat.cast_bit0` states that for any natural number `n` and any type `R` that is an add monoid with a one element, casting the bit-doubled value of `n` into `R` is the same as bit-doubling the cast of `n` into `R`. Here, the `bit0` function doubles a number by adding it to itself. In more mathematical terms, for all natural numbers `n` and any type `R` that is an add monoid with one, we have `2 * coe(n) = coe(2 * n)` where `coe` represents the casting function.
More concisely: For any natural number `n` and add monoid `R` with one, `2 * (coe n) = coe (2 * n)`.
|
Nat.cast_succ
theorem Nat.cast_succ : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ), ↑n.succ = ↑n + 1
This theorem, `Nat.cast_succ`, states that for any countable number `n` of type natural number (`ℕ`), and for any type `R` that is equipped with an addition operation and a distinguished element called `one` (which is to say, `R` is an 'additive monoid with one'), the casting of the successor of `n` (denoted by `Nat.succ n`) into `R` is equal to the sum of the cast of `n` into `R` and `1`. In other words, it translates the natural number property that the next number after `n` is `n + 1` into the context of the type `R`.
More concisely: For any countable natural number `n` and additive monoid `R` with one, `Nat.succ (Nat.cast R n) = Nat.cast R n + 1`.
|
Nat.cast_ofNat
theorem Nat.cast_ofNat :
∀ {R : Type u_1} {n : ℕ} [inst : NatCast R] [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
This theorem, named `Nat.cast_ofNat`, states that for any given type `R` and natural number `n` which is at least two (`Nat.AtLeastTwo n`), the natural number `n`, when it is cast to type `R` using the `NatCast` instance (`↑(OfNat.ofNat n)`), is equal to the result of applying the `OfNat.ofNat` function on `n`. Here, the `OfNat.ofNat` function is a method of creating elements of type `R` from natural numbers. In other words, it establishes the equivalence between two methods of converting natural numbers to other types, given that the natural number is at least two.
More concisely: For any type `R` and natural number `n` (`Nat.AtLeastTwo n`), the operation `↑(OfNat.ofNat n)` equals `OfNat.ofNat n`.
|
Mathlib.Data.Nat.Cast.Defs._auxLemma.3
theorem Mathlib.Data.Nat.Cast.Defs._auxLemma.3 :
∀ {R : Type u_1} [inst : AddMonoidWithOne R] (m n : ℕ), ↑m + ↑n = ↑(m + n)
This theorem, titled `Mathlib.Data.Nat.Cast.Defs._auxLemma.3`, states that for any type `R` that has an `AddMonoidWithOne` structure, and for any natural numbers `m` and `n`, the sum of the casts of `m` and `n` to type `R` is equal to the cast of the sum of `m` and `n` to type `R`. In mathematical terms, it asserts that `↑m + ↑n` equals `↑(m + n)`, where `↑` denotes the cast to type `R`. This essentially allows us to treat the casting function as a homomorphism when it comes to addition.
More concisely: For any type `R` with an `AddMonoidWithOne` structure and natural numbers `m` and `n`, the cast of `m + n` to type `R` is equal to the sum of the casts of `m` and `n` to type `R`. In Lean, this is expressed by `Mathlib.Data.Nat.Cast.Defs._auxLemma.3`.
|
AddMonoidWithOne.natCast_succ
theorem AddMonoidWithOne.natCast_succ :
∀ {R : Type u_2} [self : AddMonoidWithOne R] (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
This theorem states that the canonical map from the natural numbers (ℕ) to some type `R` (which is an additive monoid with a unit) is an homomorphism. In particular, it says that for all natural numbers `n`, the image of `n + 1` under this map is equal to the image of `n` under the map, incremented by one. This preserves the additive structure of the natural numbers in the target type `R`.
More concisely: The canonical map from the natural numbers to an additive monoid with a unit preserves addition, i.e., for all natural numbers n, the image of n under this map is equal to the image of n-1 plus the image of 1.
|
Nat.cast_one
theorem Nat.cast_one : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], ↑1 = 1
This theorem states that, for any type `R` that is an additive monoid with a one element (`AddMonoidWithOne R`), the natural number cast of `1` (represented as `↑1`) is equal to the one element of `R` (represented as `1`). In simpler terms, it says that casting one from natural numbers to any type with a one element and addition operation gives us the one element of that type.
More concisely: For any additive monoid with a one element `R`, the natural number `1` equals the one element `1` in `R`.
|