Nat.abs_cast
theorem Nat.abs_cast : ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a : ℕ), |↑a| = ↑a
This theorem states that for any natural number `a` and for any type `α`, which is a linear ordered ring, the absolute value of the cast of `a` to `α` is equal to the cast of `a` to `α`. In other words, it establishes that the absolute value operation doesn't affect natural numbers after being casted to a type that is a linear ordered ring.
More concisely: For any natural number `a` and any linear ordered ring `α`, the absolute value of `a` in `α` equals the cast of `a` to `α`.
|
Nat.cast_le
theorem Nat.cast_le :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
This theorem, `Nat.cast_le`, states that for any type `α` that is an additive monoid with a one element, has a partial order, satisfies the covariant class property for addition and order, has zero less than or equal to one, and has characteristic zero, the inequality between the natural number castings `m` and `n` to `α` holds if and only if the inequality between `m` and `n` holds. In other words, casting doesn't change the order of natural numbers.
More concisely: For types `α` that are additive monoids with a one element, have a partial order, satisfy the covariant class property for addition and order, have zero less than or equal to one, and have characteristic zero, the natural number castings to `α` preserve the order relation.
|
Nat.cast_pos
theorem Nat.cast_pos : ∀ {α : Type u_3} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {n : ℕ}, 0 < ↑n ↔ 0 < n := by
sorry
This theorem, `Nat.cast_pos`, is a specialized version of another theorem, `Nat.cast_pos'`. It states that for any natural number `n`, the statement "0 is less than the cast of `n` to a type `α`" is equivalent to the statement "0 is less than `n`". Here, `α` is any type that forms an ordered semiring and is nontrivial (i.e., it contains at least two distinct elements).
More concisely: For any natural number `n` and type `α` forming an ordered semiring, `0` is less than `Nat.cast (α) n` if and only if `0` is less than `n`.
|
Nat.cast_max
theorem Nat.cast_max : ∀ {α : Type u_3} [inst : LinearOrderedSemiring α] {a b : ℕ}, ↑(max a b) = max ↑a ↑b
This theorem states that for any two natural numbers, `a` and `b`, and any type `α` that forms a linear ordered semiring, the maximum of `a` and `b` when cast into type `α` is the same as the maximum of `a` and `b` when each is individually cast into `α`. In other words, it doesn't matter if you take maximum before or after the casting operation, the result will be the same.
More concisely: For any natural numbers `a` and `b` and a linear ordered semiring type `α`, the maximum of `a` and `b` in `α` is equal to the maximum of `a` and `b` each cast individually into `α`.
|
Nat.cast_lt
theorem Nat.cast_lt :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {m n : ℕ}, ↑m < ↑n ↔ m < n
This theorem states that for any type `α` that satisfies certain properties, specifically being an additive monoid with a one element, having a partial order, satisfying the covariant class property with respect to addition and less than or equal to relation, having a zero element less than or equal to the one element, and having characteristic zero, the natural number cast of `m` is less than the natural number cast of `n` if and only if `m` is less than `n`. In other words, the less than relation is preserved under the casting from natural numbers to the type `α`.
More concisely: For any additive monoid with one element, partial order, covariant class property for addition and less-than-or-equal relation, zero element less than one, and characteristic zero `α`, the natural number less-than relation is equivalent to the relation induced by natural number casts in `α`.
|
Nat.cast_pos'
theorem Nat.cast_pos' :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1] {n : ℕ}, 0 < ↑n ↔ 0 < n
This theorem states that for any natural number `n`, `n` is greater than 0 if and only if the casted `n` in some type `α` is greater than 0. Here, `α` is a type that is an additive monoid with a unit element, has a partial order, satisfies the covariant law for addition and order, includes 0 and 1 with 0 less than or equal to 1, and where 1 is not equal to 0. The casting operation is from natural numbers to `α`.
More concisely: For any natural number `n` and type `α` that is an additive monoid with a unit, has a partial order, satisfies the covariant law for addition and order, includes 0 and 1 with 0 less than 1, and where 1 is not equal to 0, the natural number `n` is greater than 0 if and only if the casted `n` in `α` is greater than its zero element.
|
Mathlib.Data.Nat.Cast.Order._auxLemma.23
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.23 :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {n : ℕ} [inst_5 : n.AtLeastTwo], (1 ≤ OfNat.ofNat n) = True
This theorem, named `Mathlib.Data.Nat.Cast.Order._auxLemma.23`, states that for any type `α` that has the structures of an additive monoid with one, a partial order, a covariant class under addition and order, a Zero to One class, and has characteristic zero, and given any natural number `n` that is at least two, the 'ofNat' cast of `n` to `α` is always greater than or equal to one. In other words, when we map a natural number `n` (where `n` is at least two) to any such structure `α`, the result is always greater than or equal to one.
More concisely: For any type `α` with the structures of an additive monoid with one, a partial order, covariance under addition and order, Zero to One class, and characteristic zero, the `ofNat` cast of any natural number `n` (where `n` is at least two) is greater than or equal to one.
|
Mathlib.Data.Nat.Cast.Order._auxLemma.11
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.11 :
∀ {α : Type u_3} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {n : ℕ} [inst_2 : n.AtLeastTwo],
(0 < OfNat.ofNat n) = True
This theorem, `Mathlib.Data.Nat.Cast.Order._auxLemma.11`, states that for any type `α` that is an instance of `OrderedSemiring` and `Nontrivial` and for any natural number `n` that is at least two, the statement that `0` is less than `n` when `n` is cast to the type `α` using the `OfNat.ofNat` function, is always true. In simpler terms, it ensures that when you cast a natural number `n` (which is at least two) to any nontrivial ordered semiring, the result is always greater than zero.
More concisely: For any `α` an instance of `OrderedSemiring` and `Nontrivial`, and `n` a natural number greater than or equal to 2, `0 < OfNat.ofNat n : α`.
|
Nat.cast_nonneg
theorem Nat.cast_nonneg : ∀ {α : Type u_3} [inst : OrderedSemiring α] (n : ℕ), 0 ≤ ↑n
This theorem, `Nat.cast_nonneg`, states that for any natural number `n` and any type `α` that is an ordered semiring, the casted value of `n` into `α` is always nonnegative, i.e., greater than or equal to zero. In other words, when we convert a natural number to any ordered semiring type, the result is guaranteed to be nonnegative. This is a specialisation of the more general `Nat.cast_nonneg'` theorem.
More concisely: For any natural number `n` and ordered semiring type `α`, the conversion of `n` to `α` results in a value that is non-negative.
|
Mathlib.Data.Nat.Cast.Order._auxLemma.22
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.22 :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {n : ℕ} [inst_5 : n.AtLeastTwo], (1 < OfNat.ofNat n) = True
The theorem `Mathlib.Data.Nat.Cast.Order._auxLemma.22` states that for any type `α`, given that `α` is an additive monoid with a unity element, has a partial order, obeys the covariant law for addition and comparison, includes a `ZeroLEOneClass` instance, and is characterized by zero, and for any natural number `n` that is at least two, the statement that "one is less than the natural number `n` cast to `α`" is always true. This theorem is particularly useful in situations where natural numbers are cast to other types, and the properties of these types are critical in reasoning about their behavior.
More concisely: For any additive monoid with a unity element, partial order, covariant law for addition and comparison, `ZeroLEOneClass` instance, and characterization of zero, one is less than any natural number cast to this type.
|
Mathlib.Data.Nat.Cast.Order._auxLemma.24
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.24 :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {n : ℕ} [inst_5 : n.AtLeastTwo], (OfNat.ofNat n ≤ 1) = False
The theorem `Mathlib.Data.Nat.Cast.Order._auxLemma.24` states that for any type `α` that is an additive monoid with a distinguished one, has a partial order, is covariant, has a zero that is less than or equal to one, has characteristic zero, and a natural number `n` that is at least two, the proposition that `n` (cast to type `α` using the `OfNat.ofNat` function) is less than or equal to `1` is always false.
More concisely: For any additive monoid α with one, partial order, covariant, zero <= 1, characteristic zero, and n >= 2, it is false that n (as an element of α) is less than or equal to 1.
|
Mathlib.Data.Nat.Cast.Order._auxLemma.13
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.13 :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {m n : ℕ}, (↑m < ↑n) = (m < n)
This theorem states that for any type `α` that is a sum monoid with an identity element, is partially ordered, fulfills covariant class conditions, has zero less than or equal to one, and has character zero, and for any natural numbers `m` and `n`, the cast of `m` to `α` is less than the cast of `n` to `α` if and only if `m` is less than `n`. This establishes a correspondence between the less-than relation in the natural numbers and the less-than relation in the structure `α` after casting the natural numbers to `α`.
More concisely: For any sum monoid with an identity element `α` that is partially ordered, covariant, has zero less than or equal to one, and has character zero, the natural number `m` is less than `n` if and only if the cast of `m` to `α` is less than the cast of `n` to `α`.
|
Nat.one_lt_cast
theorem Nat.one_lt_cast :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {n : ℕ}, 1 < ↑n ↔ 1 < n
This theorem, `Nat.one_lt_cast`, states that for any type `α` that has the structure of an additive monoid with an element designated as "one", is partially ordered, has a covariant class, has a zero less than or equal to one class, and has a character zero property, a natural number `n` is greater than 1 if and only if its typecast to `α` is also greater than 1. Essentially, it ensures the property of "being greater than 1" is preserved when casting from natural numbers to other number-like types.
More concisely: For any additive monoid type `α` with one, partial order, covariant class, zero less than or equal to one class, and character zero property, the relation "greater than 1" for natural numbers is equivalent to the relation "greater than 1" for type-casted elements of `α`.
|
Mathlib.Data.Nat.Cast.Order._auxLemma.9
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.9 :
∀ {α : Type u_3} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {n : ℕ}, (0 < ↑n) = (0 < n)
This theorem, `Mathlib.Data.Nat.Cast.Order._auxLemma.9`, states that for any ordered semiring `α` of any type `u_3`, and any non-trivial instance `α`, for a given natural number `n`, the inequality `0 < ↑n` (which represents the cast of `n` to type `α`) is equivalent to `0 < n`. In simpler terms, this theorem asserts that a natural number `n` is greater than zero if and only if its cast to an ordered semiring is also greater than zero.
More concisely: For any ordered semiring `α` and natural number `n`, `0 < ↑n` if and only if `0 < n`.
|
Nat.strictMono_cast
theorem Nat.strictMono_cast :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α], StrictMono Nat.cast
The theorem `Nat.strictMono_cast` states that for any type `α` with the structures of an `AddMonoidWithOne`, `PartialOrder`, `CovariantClass` for addition and order, `ZeroLEOneClass`, and `CharZero`, the function that casts natural numbers to `α` is strictly monotone. In other words, for any two natural numbers `a` and `b`, if `a` is strictly less than `b`, then the casting of `a` into `α` is strictly less than the casting of `b` into `α`. The `CovariantClass` ensures an interaction between the addition operation and the order relation, while `ZeroLEOneClass` and `CharZero` provide specific properties about the elements `0` and `1` in the type `α`.
More concisely: If `α` is a type with the structures of an AddMonoidWithOne, PartialOrder, CovariantClass for addition and order, ZeroLEOneClass, and CharZero, then the function that casts natural numbers to `α` is a strict monotone function with respect to the order relation on natural numbers.
|
Mathlib.Data.Nat.Cast.Order._auxLemma.12
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.12 :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {m n : ℕ}, (↑m ≤ ↑n) = (m ≤ n)
This theorem states that for any type `α` which is an additive monoid with identity, has a partial order, has a covariant class where addition induces an ordering, has a zero less than or equal to one, and has a characteristic of zero, the natural number casting of `m` to `α` being less than or equal to the natural number casting of `n` to `α` is equivalent to `m` being less than or equal to `n` in the set of natural numbers. In other words, in this specific context, the process of casting doesn't change the relative order of the natural numbers.
More concisely: For any additive monoid with identity, partial order, covariant additive ordering, zero less than one, and characteristic zero, the natural number casting function respects the order relation between natural numbers.
|
Nat.mono_cast
theorem Nat.mono_cast :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α],
Monotone Nat.cast
The theorem `Nat.mono_cast` states that for any type `α` that is an additive monoid with a one element, contains a partial order, has a covariant class with respect to addition and comparison, and includes zero and one as elements, the function that casts a natural number to that type is monotone. In other words, if `a` and `b` are natural numbers and `a ≤ b`, then casting `a` and `b` to `α` preserves this order: the cast of `a` is less than or equal to the cast of `b`.
More concisely: If `α` is an additive monoid with a one element, a partial order, covariant class with respect to addition and comparison, and includes zero and one, then the function that casts natural numbers to `α` is monotone with respect to the natural number ordering.
|
Nat.one_le_cast
theorem Nat.one_le_cast :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {n : ℕ}, 1 ≤ ↑n ↔ 1 ≤ n
This theorem states that for all types `α` which are instances of `AddMonoidWithOne`, `PartialOrder`, `CovariantClass` with respect to addition and less than or equal to relation, `ZeroLEOneClass` and `CharZero`, and for all natural numbers `n`, the statement "1 is less than or equal to the cast of `n` to `α`" is equivalent to the statement "1 is less than or equal to `n`". Hence, the comparison of 1 with a natural number `n` remains the same after `n` is cast to any type `α` satisfying the mentioned properties.
More concisely: For all types `α` instancing AddMonoidWithOne, PartialOrder, CovariantClass for addition and <= relation, ZeroLEOneClass, and CharZero, and all natural numbers `n`, 1 <= n if and only if 1 <= (cast n to α).
|
Nat.cast_add_one_pos
theorem Nat.cast_add_one_pos :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1] (n : ℕ), 0 < ↑n + 1
This theorem states that for any natural number `n`, if you have a type `α` that is an additive monoid with a unit element, has a partial order, a covariant class, respects the zero and one order, and where one is not zero, then the cast of `n` to `α` plus one is greater than zero. Essentially, this is asserting that when you add one to any non-negative natural number cast to a certain type, the result is always positive.
More concisely: For any additive monoid with a unit element, partial order, covariance, and respect for zero and one, if one is non-zero, then for all natural numbers `n`, the element `(n : α) + 1` is positive in `α`.
|
Nat.abs_ofNat
theorem Nat.abs_ofNat :
∀ {α : Type u_1} [inst : LinearOrderedRing α] (n : ℕ) [inst_1 : n.AtLeastTwo], |OfNat.ofNat n| = OfNat.ofNat n := by
sorry
The theorem `Nat.abs_ofNat` states that for any type `α` which is a LinearOrderedRing and any natural number `n` that is at least two, the absolute value of `n` as an element of `α` (which is represented by `OfNat.ofNat n`) is equal to `n` as an element of `α`. In other words, this theorem asserts that the absolute value function preserves the natural number when it is embedded into any LinearOrderedRing, as long as the natural number is at least two.
More concisely: For any LinearOrderedRing type `α` and natural number `n` ≥ 2, the absolute value of `OfNat.ofNat n` in `α` equals `n`.
|
Mathlib.Data.Nat.Cast.Order._auxLemma.4
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.4 :
∀ {α : Type u_3} [inst : OrderedSemiring α] (n : ℕ) [inst_1 : n.AtLeastTwo], (0 ≤ OfNat.ofNat n) = True
The theorem `Mathlib.Data.Nat.Cast.Order._auxLemma.4` states that for any type `α` which is an Ordered Semiring, and for any natural number `n` that is at least two, the result of casting `n` to `α` using the function `OfNat.ofNat` is always greater than or equal to zero. The equality to `True` signifies that this proposition is always true.
More concisely: For any Ordered Semiring type `α` and natural number `n` ≥ 2, `OfNat.ofNat n ≥ 0`.
|
Nat.cast_nonneg'
theorem Nat.cast_nonneg' :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α] (n : ℕ),
0 ≤ ↑n
This theorem, `Nat.cast_nonneg'`, states that for any natural number `n` and any type `α` that is an ordered semiring (a structure with addition and multiplication operations that has an additive identity "zero", a multiplicative identity "one", and a partial order defined on it), the cast of `n` to `α` is always nonnegative. In other words, casting any natural number to another type in the context of an ordered semiring will never result in a value less than zero.
More concisely: For any natural number `n` and ordered semiring `α`, the coercion from `n` to `α` is non-negative.
|
Nat.cast_tsub
theorem Nat.cast_tsub :
∀ {α : Type u_1} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (m n : ℕ), ↑(m - n) = ↑m - ↑n
The theorem `Nat.cast_tsub` states: for any canonically ordered commutative semiring `α`, which also supports subtraction operation that obeys order rules, and for any two natural numbers `m` and `n`, the operation of subtracting `n` from `m` and then casting the result to `α` is the same as the operation of casting `m` and `n` to `α` individually, subtracting these two, and then ordering the results. This theorem, however, does not hold for extended nonnegative real numbers (`ℝ≥0∞`) and extended natural numbers (`ℕ∞`).
More concisely: For any commutative semiring α with order and subtraction obeying the order rules, casting and subtracting natural numbers in α is equivalent to subtracting the casted numbers and then ordering the results. (This theorem does not hold for extended nonnegative real numbers and extended natural numbers.)
|
Mathlib.Data.Nat.Cast.Order._auxLemma.2
theorem Mathlib.Data.Nat.Cast.Order._auxLemma.2 :
∀ {α : Type u_3} [inst : OrderedSemiring α] (n : ℕ), (0 ≤ ↑n) = True
This theorem states that for any natural number `n` and any type `α` that forms an ordered semiring, the cast of `n` to `α` is always greater than or equal to zero. In mathematical terms, if we cast a natural number to a member of an ordered semiring, the result will always be non-negative.
More concisely: For any natural number `n` and ordered semiring `α`, the coercion of `n` to `α` is non-negative.
|