EuclideanDomain.gcd_eq_gcd_ab
theorem EuclideanDomain.gcd_eq_gcd_ab :
∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
EuclideanDomain.gcd a b = a * EuclideanDomain.gcdA a b + b * EuclideanDomain.gcdB a b
This theorem is an explicit version of Bézout's lemma for Euclidean domains. In particular, it states that for any Euclidean domain `R` with decidable equality and any two elements `a` and `b` in `R`, the greatest common divisor of `a` and `b` can be expressed as a linear combination of `a` and `b`. More specifically, the gcd of `a` and `b` is equal to `a` times some `a`-coefficient plus `b` times some `b`-coefficient, where these coefficients are given by `EuclideanDomain.gcdA a b` and `EuclideanDomain.gcdB a b` respectively. In mathematical terms, this is saying that $\gcd(a, b) = a \cdot \text{gcdA}(a, b) + b \cdot \text{gcdB}(a, b)$ for all `a, b` in `R`.
More concisely: In a Euclidean domain, the greatest common divisor of two elements can be expressed as their linear combination with coefficients given by the gcd coefficients from the Euclidean domain's gcd function. Equivalently, gcd(a, b) = a * gcdA(a, b) + b * gcdB(a, b) for all a, b in R.
|
EuclideanDomain.gcd_dvd_right
theorem EuclideanDomain.gcd_dvd_right :
∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R), EuclideanDomain.gcd a b ∣ b := by
sorry
The theorem `EuclideanDomain.gcd_dvd_right` states that for any type `R` that forms a Euclidean Domain and has decidable equality, for any two elements `a` and `b` in `R`, the greatest common divisor (gcd) of `a` and `b` divides `b`. This means there exists some element in `R` such that multiplying that element by the gcd of `a` and `b` yields `b`.
More concisely: For any Euclidean Domain `R` with decidable equality, the greatest common divisor of elements `a` and `b` in `R` divides `b`. In other words, `gcd a b | b` in `R`.
|
EuclideanDomain.div_self
theorem EuclideanDomain.div_self : ∀ {R : Type u} [inst : EuclideanDomain R] {a : R}, a ≠ 0 → a / a = 1
The theorem `EuclideanDomain.div_self` states that for any type `R` that is an instance of the `EuclideanDomain` class, if `a` is a non-zero element of `R`, then the division of `a` by itself equals 1. Essentially, it asserts the property of division where any non-zero number divided by itself results in 1, for any Euclidean domain.
More concisely: For any EuclideanDomain `R` and non-zero element `a` in `R`, `a / a = 1`.
|
EuclideanDomain.mul_div_assoc
theorem EuclideanDomain.mul_div_assoc :
∀ {R : Type u} [inst : EuclideanDomain R] (x : R) {y z : R}, z ∣ y → x * y / z = x * (y / z)
This theorem, named `EuclideanDomain.mul_div_assoc`, asserts a specific property of division in the context of Euclidean Domains. Specifically, for any type `R` that forms a Euclidean Domain, and for any variables `x`, `y`, and `z` of type `R`, if `z` divides `y` then the result of first multiplying `x` and `y` and then dividing by `z` is equal to the result of first dividing `y` by `z` and then multiplying the result by `x`. In mathematical notation, `x * y / z = x * (y / z)` whenever `z` divides `y`.
More concisely: For any Euclidean Domain `R` and elements `x, y, z` in `R`, if `z` divides `y`, then `x * (y / z) = (x * y) / z`.
|
EuclideanDomain.mod_eq_zero
theorem EuclideanDomain.mod_eq_zero : ∀ {R : Type u} [inst : EuclideanDomain R] {a b : R}, a % b = 0 ↔ b ∣ a
This theorem, "EuclideanDomain.mod_eq_zero", states that for all types 'R' that have a EuclideanDomain structure, and for any two elements 'a' and 'b' of this type, the remainder of 'a' divided by 'b' equals zero if and only if 'b' divides 'a'. In mathematical terms, it's saying that in a Euclidean domain, 'b' divides 'a' precisely when the remainder of the Euclidean division of 'a' by 'b' is zero.
More concisely: In a Euclidean domain, 'a' is congruent to zero modulo 'b' if and only if 'b' divides 'a'.
|
EuclideanDomain.gcd_dvd_left
theorem EuclideanDomain.gcd_dvd_left :
∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R), EuclideanDomain.gcd a b ∣ a := by
sorry
This theorem states that for any type `R` that is a Euclidean domain and has decidable equality, the greatest common divisor (gcd) of any two elements `a` and `b` of `R` divides `a`. In more mathematical terms, if `a` and `b` are elements of a Euclidean domain `R`, then the greatest common divisor of `a` and `b`, denoted by `gcd(a,b)`, is a divisor of `a`. This is a common property of greatest common divisors in number theory.
More concisely: In a Euclidean domain with decidable equality, the greatest common divisor of any two elements divides the first element.
|
EuclideanDomain.zero_div
theorem EuclideanDomain.zero_div : ∀ {R : Type u} [inst : EuclideanDomain R] {a : R}, 0 / a = 0
This theorem states that in any Euclidean domain `R`, for each element `a` in `R`, the division of `0` by `a` equals `0`. That is, it generalizes the familiar property from number theory that zero divided by any number is zero to an abstract Euclidean domain.
More concisely: In any Euclidean domain, the division of zero by any non-zero element is equal to zero.
|
EuclideanDomain.gcd_dvd
theorem EuclideanDomain.gcd_dvd :
∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b
The theorem `EuclideanDomain.gcd_dvd` states that for any type `R` which is a Euclidean domain and has decidable equality, and for any two elements `a` and `b` of this type, the greatest common divisor (gcd) of `a` and `b` divides both `a` and `b`. This means that there exist some elements in the Euclidean domain such that when they are multiplied by the gcd of `a` and `b`, they yield `a` and `b` respectively.
More concisely: For any Euclidean domain `R` with decidable equality and any elements `a` and `b` in `R`, the greatest common divisor `d` of `a` and `b` satisfies `d` | `a` and `d` | `b`. (Here, `|` denotes divisibility.)
|
EuclideanDomain.gcd_val
theorem EuclideanDomain.gcd_val :
∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
EuclideanDomain.gcd a b = EuclideanDomain.gcd (b % a) a
This theorem states that for any type `R` that forms a Euclidean domain and has decidable equality, and for any elements `a` and `b` of `R`, the greatest common divisor (gcd) of `a` and `b` is equal to the gcd of `b` modulo `a` and `a`. This is a property of Euclidean domains and is a key part of the Euclidean algorithm for computing the gcd of two elements.
More concisely: In a Euclidean domain with decidable equality, the gcd of `a` and `b` equals the gcd of `b` modulo `a` and `a`.
|