Rat.cast_div
theorem Rat.cast_div : ∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α] (m n : ℚ), ↑(m / n) = ↑m / ↑n
This theorem, `Rat.cast_div`, states that for any type `α`, given that `α` has a division ring structure and its characteristic is zero, the division of any two rational numbers `m` and `n` (expressed as `m / n`) when cast to `α` is equal to the division of `m` cast to `α` and `n` cast to `α` (expressed as `↑m / ↑n`). Essentially, this theorem ensures that the division operation in the rational numbers can be correctly translated into the division operation in other numeric types with a division ring structure and zero characteristic.
More concisely: For any type `α` with a division ring structure and characteristic zero, the operation `m / n` of rational numbers is equal to the operation `↑m / ↑n` of `α`, where `m` and `n` are rational numbers and `↑` denotes the coercion from rational numbers to `α`.
|
Mathlib.Data.Rat.Cast.CharZero._auxLemma.1
theorem Mathlib.Data.Rat.Cast.CharZero._auxLemma.1 :
∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α] {m n : ℚ}, (↑m = ↑n) = (m = n)
This theorem states that for any type `α` which is a `DivisionRing` and has a characteristic of zero (denoted by `CharZero α`), and for any rational numbers `m` and `n`, the condition that the cast of `m` to `α` equals the cast of `n` to `α` is equivalent to `m` being equal to `n`. In other words, it says that if two rational numbers are equal, then their cast to any division ring with characteristic zero will also be equal, and vice versa.
More concisely: For any division ring `α` of characteristic zero, the cast function from the rational numbers to `α` is a ring homomorphism preserving equalities.
|
Rat.cast_inv
theorem Rat.cast_inv : ∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α] (n : ℚ), ↑n⁻¹ = (↑n)⁻¹
This theorem states that for any rational number `n`, the reciprocal of the cast of `n` to a division ring `α` (where `α` is of characteristic zero) is equal to the cast of the reciprocal of `n` to `α`. In other words, taking the reciprocal then casting is the same operation as casting then taking the reciprocal. This theorem is valid for any type `α` as long as `α` forms a division ring and its characteristic is zero.
More concisely: For any rational number `n` and any division ring `α` of characteristic zero, the cast of the reciprocal of `n` to `α` equals the reciprocal of the cast of `n` to `α`.
|
Rat.cast_add
theorem Rat.cast_add : ∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α] (m n : ℚ), ↑(m + n) = ↑m + ↑n
This theorem states that for any two rational numbers `m` and `n`, the operation of casting their sum to a type `α` (which is a division ring with characteristic zero) is the same as individually casting `m` and `n` to type `α` first and then adding them. In other words, it asserts the commutativity of addition and the cast operation for rational numbers in a division ring with characteristic zero.
More concisely: For any rational numbers m and n, the conversion of their sum to a division ring with characteristic zero is equal to the sum of their individual conversions.
|
Rat.cast_inj
theorem Rat.cast_inj : ∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α] {m n : ℚ}, ↑m = ↑n ↔ m = n := by
sorry
This theorem states that given any type `α` which is a division ring and has a characteristic of zero, for any two rational numbers `m` and `n`, the condition of their casted values (to the type `α`) being equal is equivalent to the condition of `m` and `n` being equal. Here, casting refers to the operation of changing one data type into another, in this case, from rational numbers to any type `α` which is a division ring with characteristic zero. In simple words, for this specific kind of type `α`, if the casted values of two rational numbers are equal, then the two rational numbers are also equal.
More concisely: For any division ring `α` of characteristic zero, the function `α.cast` from the rational numbers to `α` is a bijection.
|
Rat.cast_injective
theorem Rat.cast_injective :
∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α], Function.Injective Rat.cast
The theorem `Rat.cast_injective` states that for any type `α` that is a DivisionRing and has a "characteristic zero" property (expressed by the typeclass `CharZero`), the canonical homomorphism from rational numbers to `α` (denoted by the function `Rat.cast`) is injective. In other words, if `Rat.cast` maps two rational numbers to the same element of `α`, then these two rational numbers were the same to begin with. This property is fundamental in the field of number theory and algebra.
More concisely: The canonical homomorphism from rational numbers to a DivisionRing of characteristic zero preserves equalities.
|
Rat.cast_sub
theorem Rat.cast_sub : ∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α] (m n : ℚ), ↑(m - n) = ↑m - ↑n
This theorem, named `Rat.cast_sub`, states that for any type `α` which is a division ring with characteristic zero, the action of casting the difference of two rational numbers `m` and `n` to the type `α` is equal to the difference of the castings of `m` and `n` to the type `α`. In more mathematical terms, it says that if `m` and `n` are rational numbers and `α` is a division ring with characteristic zero, then `(m - n)` cast to `α` is equal to `m` cast to `α` minus `n` cast to `α`. This property is often known as the preservation of subtraction under casting.
More concisely: For any division ring `α` with characteristic zero, the operation of casting the difference of two rational numbers to `α` is equal to the difference of casting each rational number to `α`.
|
Rat.cast_mul
theorem Rat.cast_mul : ∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α] (m n : ℚ), ↑(m * n) = ↑m * ↑n
This theorem states that for any type `α` that is a division ring and has property `CharZero`, the casting of the product of two rational numbers `m` and `n` to type `α` is equal to the product of the castings of `m` and `n` to type `α`. In mathematical terms, it asserts that the map from the rationals to `α` preserves multiplication, i.e., for any rational numbers `m` and `n`, `(m * n)` cast to `α` is same as `(m cast to α) * (n cast to α)`.
More concisely: For any division ring α with CharZero property, the multiplication homomorphism from the rationals to α holds, that is, (m * n) cast to α = (m cast to α) * (n cast to α) for all rational numbers m and n.
|
Mathlib.Data.Rat.Cast.CharZero._auxLemma.3
theorem Mathlib.Data.Rat.Cast.CharZero._auxLemma.3 :
∀ {α : Type u_3} [inst : DivisionRing α] [inst_1 : CharZero α] (m n : ℚ), ↑m + ↑n = ↑(m + n)
This theorem takes a type `α`, which is a division ring and has characteristic zero, along with two rational numbers `m` and `n`. It states that the sum of the casted values of `m` and `n` to the type `α` is equal to the casted value of the sum of `m` and `n` to the type `α`. In other words, the process of casting from rationals to type `α` preserves the addition operation. This can be expressed mathematically as: if `m` and `n` are rational numbers and `α` is a type with certain properties, then `↑m + ↑n = ↑(m + n)`.
More concisely: If `α` is a division ring of characteristic zero, then for all rational numbers `m` and `n`, `↑(m + n) = ↑m + ↑n`, where `↑` denotes casting from rationals to type `α`.
|