Rat.cast_one
theorem Rat.cast_one : ∀ {α : Type u_3} [inst : DivisionRing α], ↑1 = 1
This theorem states that for any type `α` which is a Division Ring, casting the rational number `1` to this type results in the number `1` in that type. Simply put, in any Division Ring, the representation of the rational number `1` is also `1`.
More concisely: In any division ring, the rational number 1 is equal to its multiplicative identity of the same type.
|
eq_ratCast
theorem eq_ratCast :
∀ {F : Type u_1} {α : Type u_3} [inst : DivisionRing α] [inst_1 : FunLike F ℚ α] [inst_2 : RingHomClass F ℚ α]
(f : F) (q : ℚ), f q = ↑q
The theorem `eq_ratCast` states that for all types `F` and `k`, where `k` is a division ring, `F` is a type which fits the `FunLike` class (i.e., terms of type `F` can be mapped injectively into functions from rational numbers `ℚ` to `k`), and `F` also fits the `RingHomClass` (i.e., type `F` creates ring homomorphisms from rational numbers `ℚ` to `k`), then for all elements `f` of type `F` and rational numbers `r`, the application of `f` on `r` equals the cast of `r` into type `k`. In simple terms, if `f` represents a ring homomorphism, then applying `f` to a rational number `r` is the same as casting `r` to the ring `k`.
More concisely: For any division ring `k`, given a type `F` that is both FunLike and RingHomClass over `k`, and for any `F` element `f` and rational number `r`, `f r = cast r to k`.
|
MonoidWithZeroHom.ext_rat
theorem MonoidWithZeroHom.ext_rat :
∀ {M₀ : Type u_5} [inst : MonoidWithZero M₀] {f g : ℚ →*₀ M₀},
f.comp ↑(Int.castRingHom ℚ) = g.comp ↑(Int.castRingHom ℚ) → f = g
This theorem, named `MonoidWithZeroHom.ext_rat`, states that for any type `M₀` that is a monoid with zero, if two monoid with zero homomorphisms `f` and `g` from the rational numbers (ℚ) to `M₀` agree on the integers (ℤ) - that is, if their composition with the ring homomorphism from integers to rational numbers are equal - then `f` and `g` are identical.
In other words, the homomorphisms `f` and `g` are completely determined by their action on integers. This is useful in situations where we only know the behavior of `f` and `g` on integers, and want to extend this to all rational numbers.
More concisely: Given two monoid homomorphisms from the rational numbers to a monoid with zero, if they agree on integers, then they are equal.
|
Rat.cast_coe_int
theorem Rat.cast_coe_int : ∀ {α : Type u_3} [inst : DivisionRing α] (n : ℤ), ↑↑n = ↑n
This theorem, `Rat.cast_coe_int`, serves as an alias for `Rat.cast_intCast`. It asserts that for any integer `n` and any type `α` that is a division ring, the double cast of `n` to a rational number and then to an element of `α` is the same as the direct cast of `n` to `α`. In mathematical notation, this can be written as ∀n ∈ ℤ, ∀α such that α is a division ring, ((n : ℚ) : α) = (n : α).
More concisely: For any integer `n` and division ring `α`, the direct cast of `n` to `α` is equal to the double cast of `n` first to rational numbers and then to `α`.
|
MonoidWithZeroHom.ext_rat_on_pnat
theorem MonoidWithZeroHom.ext_rat_on_pnat :
∀ {F : Type u_1} {M₀ : Type u_5} [inst : MonoidWithZero M₀] [inst_1 : FunLike F ℚ M₀]
[inst : MonoidWithZeroHomClass F ℚ M₀] {f g : F}, f (-1) = g (-1) → (∀ (n : ℕ), 0 < n → f ↑n = g ↑n) → f = g
This theorem states that for any two morphisms `f` and `g` of a type `F`, where `F` is a function that behaves like a function from the set of rational numbers ℚ to another type `M₀` equipped with the structures of monoid and zero (hence `MonoidWithZero`), then these two morphisms are identical if they give the same output when input is `-1`, and they give the same output when they are applied to any positive natural number `n`. This essentially tells us that the behavior of the morphisms `f` and `g` on `-1` and positive natural numbers fully determines these morphisms.
More concisely: If two morphisms `f` and `g` of a monoid with zero `F` from the rational numbers to a type `M₀` agree on `-1` and for all positive natural numbers `n`, then `f` and `g` are equal.
|
map_ratCast
theorem map_ratCast :
∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : DivisionRing α]
[inst_2 : DivisionRing β] [inst_3 : RingHomClass F α β] (f : F) (q : ℚ), f ↑q = ↑q
The theorem `map_ratCast` states that for any types `F`, `α`, and `β`, given an instance of `FunLike` from `α` to `β`, two instances of `DivisionRing` for `α` and `β`, and an instance of `RingHomClass` for `F` from `α` to `β`, for any function `f : F` and any rational number `q : ℚ`, the application of `f` to the cast of `q` to type `α` (denoted by `f ↑q`) is equal to the cast of `q` to type `β` (denoted by `↑q`). In other words, casting a rational number and then applying a function from a ring homomorphism class behaves the same as directly casting the rational to the target type.
More concisely: For any types `α`, `β`, a `FunLike` map `F` from `α` to `β`, and instances of `DivisionRing` for `α` and `β` and `RingHomClass` for `F` from `α` to `β`, the application of `F` to the cast of a rational number `q` to type `α` is equal to the cast of `q` to type `β`, i.e., `F ↑q = ↑q`.
|
RingHom.ext_rat
theorem RingHom.ext_rat :
∀ {F : Type u_1} {R : Type u_5} [inst : Semiring R] [inst_1 : FunLike F ℚ R] [inst : RingHomClass F ℚ R] (f g : F),
f = g
This theorem states that any two ring homomorphisms from the field of rational numbers (`ℚ`) to a semiring (`R`) are identical. This equality holds true under the conditions that the type `R` has a semiring structure, and `F` is a type that behaves like a function from `ℚ` to `R` and is equipped with the structure of a ring homomorphism. If `R` is a division ring, this theorem can be deduced from the `eq_ratCast` lemma.
More concisely: Any two ring homomorphisms from the field of rational numbers to a semiring are equal.
|
Rat.cast_coe_nat
theorem Rat.cast_coe_nat : ∀ {α : Type u_3} [inst : DivisionRing α] (n : ℕ), ↑↑n = ↑n
This theorem, known as `Rat.cast_coe_nat`, is an alias of `Rat.cast_natCast`. It states that for any division ring α and any natural number `n`, the double coercion of `n` to rational numbers and then to elements of α is the same as the direct coercion of `n` to elements of α. In simpler terms, it's asserting that casting a natural number to a rational and then to any element of a division ring is equivalent to casting the natural number directly to that division ring.
More concisely: For any division ring α and natural number n, the coercion of n to α via the rational numbers is equal to the direct coercion of n to α.
|
MonoidWithZeroHom.ext_rat'
theorem MonoidWithZeroHom.ext_rat' :
∀ {F : Type u_1} {M₀ : Type u_5} [inst : MonoidWithZero M₀] [inst_1 : FunLike F ℚ M₀]
[inst : MonoidWithZeroHomClass F ℚ M₀] {f g : F}, (∀ (m : ℤ), f ↑m = g ↑m) → f = g
This theorem `MonoidWithZeroHom.ext_rat'` states that for any two objects `f` and `g` of type `F`, both mapping from rational numbers to a `MonoidWithZero` type `M₀`, if `f` and `g` agree on all integer values (that is, for any integer `m`, the result of applying `f` to `m` is equal to the result of applying `g` to `m`), then `f` and `g` are the same. Here `FunLike F ℚ M₀` ensures `F` acts like a function from `ℚ` to `M₀`, and `MonoidWithZeroHomClass F ℚ M₀` ensures `F` respects the monoid with zero structure from `ℚ` to `M₀`.
More concisely: If two functions from rational numbers to a `MonoidWithZero` type agree on all integers, then they are equal.
|
Rat.cast_zero
theorem Rat.cast_zero : ∀ {α : Type u_3} [inst : DivisionRing α], ↑0 = 0
This theorem states that for any type `α` which is a `DivisionRing`, the rational number zero (denoted as `↑0`) is equivalent to the zero of type `α` (denoted as `0`). In simple terms, it says that casting the rational number zero to any division ring type yields the zero element of that type.
More concisely: For any division ring type `α`, the rational number zero `↑0` maps to the zero element `0` of type `α`.
|
Rat.cast_neg
theorem Rat.cast_neg : ∀ {α : Type u_3} [inst : DivisionRing α] (q : ℚ), ↑(-q) = -↑q
The theorem `Rat.cast_neg` states that for all types `α` in the division ring `α`, for any rational number `n`, the negation of `n` cast to type `α` is equal to the negation of `n` cast to type `α`. In other words, negating a rational number and then casting it to another type has the same result as first casting the rational number to another type and then negating it.
More concisely: For any type `α` in a division ring and rational number `n`, `-(Rat.cast _ α n) = Rat.cast _ α (-n)`.
|