EuclideanDomain.div_add_mod
theorem EuclideanDomain.div_add_mod : ∀ {R : Type u} [inst : EuclideanDomain R] (a b : R), b * (a / b) + a % b = a := by
sorry
This theorem is stating a property of Euclidean Domains. For any Euclidean Domain `R` and any two elements `a` and `b` of `R`, the equation `b * (a / b) + a % b = a` holds. This is very much like the division algorithm in integers where the remainder when `a` is divided by `b` added to the product of `b` and the quotient of `a` divided by `b`, gives back `a`.
More concisely: In a Euclidean domain, the quotient and remainder of any two elements satisfy the equation `b * (a / b) + a % b = a`.
|
EuclideanDomain.quotient_zero
theorem EuclideanDomain.quotient_zero :
∀ {R : Type u} [self : EuclideanDomain R] (a : R), EuclideanDomain.quotient a 0 = 0
This theorem states that in any Euclidean domain `R`, division of any element `a` by zero always yields zero. This is a convention adopted within the structure of Euclidean domain to handle such divisions. In mathematical terms, for all `a` in `R`, `a / 0 = 0`.
More concisely: In any Euclidean domain, the division of any element by zero is equal to zero.
|
EuclideanDomain.mul_left_not_lt
theorem EuclideanDomain.mul_left_not_lt :
∀ {R : Type u} [self : EuclideanDomain R] (a : R) {b : R}, b ≠ 0 → ¬EuclideanDomain.r (a * b) a
This theorem states that in a Euclidean Domain, for any given element `a` and any non-zero element `b`, the well-founded relation `r` does not hold between the product of `a` and `b` (i.e., `a * b`) and `a`. Essentially, this says that, within a Euclidean Domain, you cannot have `r(a * b, a)` be true if `b` is non-zero.
More concisely: In a Euclidean Domain, for all non-zero elements `a` and `b`, `a * b` is not related to `a` under the well-founded relation `r`.
|
EuclideanDomain.mod_zero
theorem EuclideanDomain.mod_zero : ∀ {R : Type u} [inst : EuclideanDomain R] (a : R), a % 0 = a
This theorem states that for any type `R` that forms a Euclidean Domain, the modulus of any element `a` of type `R` and `0` is `a`. In other words, if you take any element from a Euclidean Domain and compute the remainder of its division by zero, you will always get the original element back. This is expressed in the language of the Lean Theorem Prover.
More concisely: In a Euclidean Domain, for all elements `a`, `a % 0 = a`. (Here, `%` denotes modulo operation.)
|
EuclideanDomain.quotient_mul_add_remainder_eq
theorem EuclideanDomain.quotient_mul_add_remainder_eq :
∀ {R : Type u} [self : EuclideanDomain R] (a b : R),
b * EuclideanDomain.quotient a b + EuclideanDomain.remainder a b = a
This theorem, named `EuclideanDomain.quotient_mul_add_remainder_eq`, states that for any type `R` that has a EuclideanDomain structure, and for any two elements `a` and `b` of that type, the multiplication of `b` and the quotient of `a` divided by `b`, plus the remainder of `a` divided by `b`, equals `a`. This property connects the quotient and remainder functions, and it's crucial for computing the Greatest Common Divisors (GCDs) and Least Common Multiples (LCMs) in a Euclidean domain. In mathematical notation, this can be written as `b * (a / b) + a % b = a`.
More concisely: For any Euclidean domain `R` and elements `a, b` in `R`, `b * (a \ divide b) + a % b = a`.
|
EuclideanDomain.gcd_zero_left
theorem EuclideanDomain.gcd_zero_left :
∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a : R), EuclideanDomain.gcd 0 a = a
This theorem, named `EuclideanDomain.gcd_zero_left`, states that for any type `R` that is an instance of a `EuclideanDomain` and has decidable equality, the greatest common divisor (gcd) of 0 and any element `a` of `R` is `a` itself. This aligns with the definition of the gcd in number theory, where the gcd of 0 and a number is the number itself.
More concisely: For any EuclideanDomain `R` with decidable equality, the greatest common divisor of 0 and any element `a` in `R` is equal to `a`.
|
EuclideanDomain.r_wellFounded
theorem EuclideanDomain.r_wellFounded : ∀ {R : Type u} [self : EuclideanDomain R], WellFounded EuclideanDomain.r := by
sorry
This theorem states that for any type `R` that has a `EuclideanDomain` structure, the relation `r` defined on this `EuclideanDomain` is well-founded. This property is important to ensure the termination of the Greatest Common Divisor (GCD) algorithm. In other words, this theorem guarantees that if we run the GCD algorithm in a Euclidean domain, it will eventually reach a conclusion and not run indefinitely.
More concisely: The relation induced by division with remainder in a Euclidean domain is well-founded.
|
EuclideanDomain.GCD.induction
theorem EuclideanDomain.GCD.induction :
∀ {R : Type u} [inst : EuclideanDomain R] {P : R → R → Prop} (a b : R),
(∀ (x : R), P 0 x) → (∀ (a b : R), a ≠ 0 → P (b % a) a → P a b) → P a b
The theorem `EuclideanDomain.GCD.induction` states that for any type `R` that is an instance of a Euclidean domain, for any property `P` involving two elements of `R`, and for any two elements `a` and `b` of `R`, if `P` holds for 0 and any other element `x` of `R`, and if whenever `a` is not zero and `P` holds for the remainder of `b` divided by `a` and `a`, then `P` holds for `a` and `b`. This theorem is a form of mathematical induction related to the Euclidean algorithm for computing the greatest common divisor.
More concisely: If `R` is a Euclidean domain and `P` is a property that holds for any two elements `a` and `b` when `a = 0` or `a` divides `b`, then `P` holds for `gcd(a, b)`.
|
EuclideanDomain.remainder_lt
theorem EuclideanDomain.remainder_lt :
∀ {R : Type u} [self : EuclideanDomain R] (a : R) {b : R},
b ≠ 0 → EuclideanDomain.r (EuclideanDomain.remainder a b) b
The theorem `EuclideanDomain.remainder_lt` states that for any type `R` that forms a Euclidean Domain, and for any elements `a` and `b` of `R` with `b` not equal to zero, the relation `r` holds between the remainder of `a` divided by `b` and `b`. In mathematical terms, it means that for all `a` and `b` in `R`, if `b` is not zero, then the relation `r(a % b, b)` is true, where `%` denotes the remainder operation. This relation is a well-founded relation in the Euclidean Domain, ensuring the termination of the GCD algorithm.
More concisely: In a Euclidean Domain, for all non-zero elements `a` and `b`, the remainder of `a` divided by `b` is less than `b`.
|
EuclideanDomain.mod_lt
theorem EuclideanDomain.mod_lt :
∀ {R : Type u} [inst : EuclideanDomain R] (a : R) {b : R}, b ≠ 0 → EuclideanDomain.r (a % b) b
This theorem states that for any type `R` having the structure of a Euclidean Domain, and for any elements `a` and `b` of `R` where `b` is not zero, the relation `EuclideanDomain.r` holds between the modulus of `a` and `b` and `b` itself. This captures the property of the Euclidean algorithm where the remainder of division (`a % b`) is less than the divisor (`b`). In essence, this is the well-foundedness condition that ensures the Euclidean algorithm always terminates.
More concisely: For any Euclidean Domain `R` and non-zero elements `a` and `b` in `R`, the relation `|a| >= |b|` implies `|a mod b| < |b|`.
|
EuclideanDomain.div_zero
theorem EuclideanDomain.div_zero : ∀ {R : Type u} [inst : EuclideanDomain R] (a : R), a / 0 = 0
This theorem states that in a Euclidean domain `R`, the division of any element `a` by zero is equal to zero. In other words, for all elements `a` in the Euclidean domain `R`, `a / 0` equals `0`. This rule is familiar from conventional number systems, but here it's explicitly stated for any Euclidean domain, which is a type of mathematical structure that generalizes some properties of the integers.
More concisely: In a Euclidean domain, the division of any element by zero is equal to the additive identity (zero).
|