IsCoprime.add_mul_left_right
theorem IsCoprime.add_mul_left_right :
∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime x (y + x * z)
This theorem states that for any commutative ring `R` and any elements `x`, `y`, and `z` of `R`, if `x` and `y` are coprime, then `x` is also coprime with the element `y + x * z`. Here, two elements are said to be coprime if there exist two other elements in the ring such that their linear combination equals one, i.e., there exist `a` and `b` in `R` such that `a * x + b * y = 1`.
More concisely: If `x` and `y` are coprime elements in a commutative ring `R`, then `x` is coprime with `y + x * z` for any `z` in `R`.
|
IsRelPrime.of_add_mul_left_right
theorem IsRelPrime.of_add_mul_left_right :
∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime x (y + x * z) → IsRelPrime x y
The theorem `IsRelPrime.of_add_mul_left_right` states that for all types `R` that have an instance of a commutative semiring, and for all elements `x`, `y`, and `z` of `R`, if `x` and `y + x * z` are relatively prime (meaning that every common divisor of `x` and `y + x * z` is a unit), then `x` and `y` are also relatively prime. This theorem essentially tells us that the relative primality between two elements in a commutative semiring is preserved when adding a multiple of one element to the other.
More concisely: If `x` and `y + x * z` are relatively prime in a commutative semiring, then `x` and `y` are relatively prime.
|
IsCoprime.ne_zero
theorem IsCoprime.ne_zero :
∀ {R : Type u} [inst : CommSemiring R] [inst_1 : Nontrivial R] {p : Fin 2 → R}, IsCoprime (p 0) (p 1) → p ≠ 0 := by
sorry
The theorem states that given a 2-vector `p` in a commutative semiring `R` that is non-trivial (i.e., there are at least two distinct elements in `R`), if the first and second elements of `p` (accessed by `p 0` and `p 1` respectively) are coprime (meaning there exist two elements `a` and `b` in `R` such that `a * p(0) + b * p(1) = 1`), then `p` cannot be the zero vector.
More concisely: If `p` is a non-zero 2-vector in a commutative semiring `R` with coprime first and second components, then `p` is not the zero vector.
|
IsCoprime.of_add_mul_left_left
theorem IsCoprime.of_add_mul_left_left :
∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (x + y * z) y → IsCoprime x y
The theorem `IsCoprime.of_add_mul_left_left` states that for any commutative semiring `R` and any elements `x`, `y`, and `z` of `R`, if `x + y * z` and `y` are coprime, then `x` and `y` are also coprime. This is stated in the context of an arbitrary commutative semiring, which is a type of algebraic structure that includes familiar number systems like the natural numbers, integers, and rational numbers. Here, being coprime is defined as the existence of two elements `a` and `b` such that `a * x + b * y = 1`.
More concisely: If `x + y * z` and `y` are coprime elements in a commutative semiring `R`, then `x` and `y` are coprime.
|
IsCoprime.of_mul_right_left
theorem IsCoprime.of_mul_right_left :
∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (y * z) → IsCoprime x y
This theorem states that for any commutative semiring `R` and any elements `x`, `y`, and `z` of `R`, if `x` and `y * z` are coprime, then `x` and `y` are also coprime. Here, two elements are considered coprime if there exist two other elements such that their linear combination equals one.
More concisely: If `x` and `y` are elements of a commutative semiring `R` such that `x` and `y * z` are coprime for some `z` in `R`, then `x` and `y` are coprime.
|
isCoprime_comm
theorem isCoprime_comm : ∀ {R : Type u} [inst : CommSemiring R] {x y : R}, IsCoprime x y ↔ IsCoprime y x
This theorem states that the property of being coprime is commutative for any two elements `x` and `y` in a commutative semiring `R`. In other words, `x` and `y` being coprime implies `y` and `x` are also coprime, and vice versa. Here, two elements are defined as coprime if there exist two other elements `a` and `b` such that `a * x + b * y = 1`.
More concisely: In a commutative semiring, x and y being coprime is equivalent to y and x being coprime.
|
IsCoprime.isUnit_of_dvd'
theorem IsCoprime.isUnit_of_dvd' :
∀ {R : Type u} [inst : CommSemiring R] {a b x : R}, IsCoprime a b → x ∣ a → x ∣ b → IsUnit x
This theorem states that for any type `R` that is a commutative semiring, and any elements `a`, `b`, and `x` of this type, if `a` and `b` are coprime (that is, there exist two elements whose multiplication with `a` and `b` respectively, when added, equal 1), and `x` divides both `a` and `b`, then `x` is a unit. In the context of a monoid, an element is a unit if it has a two-sided inverse. Consequently, this theorem essentially claims that any number that divides two coprime numbers must have a multiplicative inverse.
More concisely: In a commutative semiring, if two coprime elements have a common divisor, then each of them is a unit of the semiring.
|
IsCoprime.of_mul_left_left
theorem IsCoprime.of_mul_left_left :
∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (x * y) z → IsCoprime x z
This theorem states that for any commutative semiring `R` and any elements `x`, `y`, and `z` of `R`, if `x * y` and `z` are coprime, then `x` and `z` are also coprime. In other words, if there exist two elements `a` and `b` in `R` such that `a * (x * y) + b * z = 1`, then there must also exist two elements `c` and `d` in `R` such that `c * x + d * z = 1`.
More concisely: If `x`, `y`, and `z` are elements of a commutative semiring `R` such that `x * y` and `z` are coprime, then `x` and `z` are also coprime, i.e., there exist `a`, `b` in `R` with `a * (x * y) + b * z = 1` implies there exist `c`, `d` in `R` with `c * x + d * z = 1`.
|
IsCoprime.of_add_mul_left_right
theorem IsCoprime.of_add_mul_left_right :
∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x (y + x * z) → IsCoprime x y
The theorem `IsCoprime.of_add_mul_left_right` states that for all types `R` that are commutative semirings, and for all elements `x`, `y`, and `z` of `R`, if `x` and `y + x * z` are coprime, then `x` and `y` are also coprime. Here, two elements are said to be coprime if there exist two other elements `a` and `b` such that `a * x + b * y = 1`.
More concisely: If `x` and `(y + x * z)` are coprime in a commutative semiring `R`, then `x` and `y` are coprime.
|
IsRelPrime.of_add_mul_left_left
theorem IsRelPrime.of_add_mul_left_left :
∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsRelPrime (x + y * z) y → IsRelPrime x y
The theorem `IsRelPrime.of_add_mul_left_left` states that for any commutative semiring `R`, and for any elements `x`, `y`, and `z` of `R`, if `x + y * z` and `y` are relatively prime, then `x` and `y` are also relatively prime. In this context, two elements being relatively prime means that any common divisor of the two is a unit.
More concisely: If `x`, `y` are elements of a commutative semiring `R` such that `y` is a common divisor of `x` and `x + y*z` for some `z` in `R`, then `y` is a unit in `R` if and only if `x` and `y` are relatively prime.
|
isCoprime_one_right
theorem isCoprime_one_right : ∀ {R : Type u} [inst : CommSemiring R] {x : R}, IsCoprime x 1
This theorem states that for any commutative semiring `R` and for any element `x` from `R`, `x` and `1` are coprime. Here, two elements `x` and `y` of a commutative semiring `R` are said to be coprime if there exist two elements `a` and `b` in `R` such that `a * x + b * y = 1`. In this case, since `1` is the multiplicative identity in `R`, every element `x` in `R` is coprime with `1`.
More concisely: In any commutative semiring, every element is coprime with the multiplicative identity.
|
IsRelPrime.add_mul_left_left
theorem IsRelPrime.add_mul_left_left :
∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime (x + y * z) y
The theorem `IsRelPrime.add_mul_left_left` states that for any commutative ring `R`, and any elements `x`, `y`, and `z` of `R`, if `x` and `y` are relatively prime (that is, their only common divisors are units), then `x + y * z` and `y` are also relatively prime. In other words, multiplying `y` by any element `z` and adding the result to `x` does not introduce any new common divisors with `y`, other than the units.
More concisely: If `x` and `y` are relatively prime elements in a commutative ring `R`, then `x` and `y + x * z` are relatively prime for all `z` in `R`.
|
IsCoprime.neg_left
theorem IsCoprime.neg_left : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → IsCoprime (-x) y
This theorem states that for any type 'R' that forms a commutative ring (denoted as `CommRing R`), if two elements `x` and `y` of type 'R' are coprime (as per the definition `IsCoprime`), then the negation of `x` (denoted as `-x`) and `y` are also coprime. This implies that if there exist two numbers `a` and `b` such that `a * x + b * y = 1`, then there also exist numbers (possibly different) such that they multiply with `-x` and `y` to give `1`.
More concisely: If `R` is a commutative ring and `x` and `y` are coprime elements of `R`, then `-x` and `y` are also coprime. That is, if `x` and `y` have no common factors besides 1, then `-x` and `y` also have no common factors besides 1.
|
IsCoprime.symm
theorem IsCoprime.symm : ∀ {R : Type u} [inst : CommSemiring R] {x y : R}, IsCoprime x y → IsCoprime y x
The theorem `IsCoprime.symm` states that the property of being coprime is symmetric. In other words, for any type `R` that has a commutative semiring structure, and any elements `x` and `y` of `R`, if `x` and `y` are coprime, then `y` and `x` are also coprime. Here, being coprime is defined as the existence of a pair of elements `a` and `b` in `R` such that `a * x + b * y = 1`.
More concisely: If `x` and `y` are coprime elements in a commutative semiring `R`, then `y` and `x` are also coprime. Equivalently, the existence of `a` and `b` in `R` such that `a * x + b * y = 1` implies the existence of `c` and `d` in `R` such that `c * y + d * x = 1`.
|
IsRelPrime.add_mul_right_left
theorem IsRelPrime.add_mul_right_left :
∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime (x + z * y) y
The theorem `IsRelPrime.add_mul_right_left` states that for any type `R` that forms a commutative ring, for any elements `x`, `y` and `z` of `R`, if `x` and `y` are relatively prime, then `x + z * y` and `y` are also relatively prime. Here, two elements are said to be relatively prime if any common divisor of them is a unit.
More concisely: If `x` and `y` are relatively prime elements in a commutative ring `R`, then `x` and `x + y * z` are relatively prime for any `z` in `R`.
|
not_isCoprime_zero_zero
theorem not_isCoprime_zero_zero : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : Nontrivial R], ¬IsCoprime 0 0 := by
sorry
This theorem states that for any commutative semiring `R` that is nontrivial (i.e., not every element is the same), the elements `0` and `0` are not coprime. In mathematical terms, it means that there do not exist elements `a` and `b` in the semiring such that `a * 0 + b * 0 = 1`.
More concisely: In any commutative nontrivial semiring, 0 is not coprime with itself.
|
isCoprime_group_smul_left
theorem isCoprime_group_smul_left :
∀ {R : Type u_1} {G : Type u_2} [inst : CommSemiring R] [inst_1 : Group G] [inst_2 : MulAction G R]
[inst_3 : SMulCommClass G R R] [inst_4 : IsScalarTower G R R] (x : G) (y z : R),
IsCoprime (x • y) z ↔ IsCoprime y z
The theorem `isCoprime_group_smul_left` states that for any types `R` and `G`, where `R` is a commutative semiring and `G` is a group, and for any scalar multiplication (`MulAction`) of `G` on `R` that commutes (`SMulCommClass`) and forms a scalar tower (`IsScalarTower`), for any elements `x` in `G` and `y`, `z` in `R`, `y` and `z` are coprime if and only if `x` times `y` (denoted as `x • y`) and `z` are coprime. This essentially states the property that the coprimality of `y` and `z` is invariant under the scaling of `y` by any element from the group `G`.
More concisely: For any commutative semiring `R`, group `G`, and a commuting, scalar tower multiplication action of `G` on `R`, if `x` is an element of `G` and `y`, `z` are coprime elements of `R`, then `x • y` and `z` are coprime.
|
isCoprime_zero_right
theorem isCoprime_zero_right : ∀ {R : Type u} [inst : CommSemiring R] {x : R}, IsCoprime x 0 ↔ IsUnit x
The theorem `isCoprime_zero_right` states that for any commutative semiring `R` and any element `x` of `R`, `x` and `0` are coprime if and only if `x` is a unit. In mathematical terms, this means there exist elements `a` and `b` in `R` such that `a * x + b * 0 = 1` if and only if there exists a two-sided inverse of `x`. Essentially, an element is coprime with zero in a commutative semiring if and only if it is invertible.
More concisely: In a commutative semiring, an element is coprime to zero if and only if it is a unit.
|
IsCoprime.mul_left
theorem IsCoprime.mul_left :
∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x z → IsCoprime y z → IsCoprime (x * y) z
The theorem `IsCoprime.mul_left` states that for any type `R` that is a commutative semiring, if `x` and `z` are coprime and `y` and `z` are coprime, then the product of `x` and `y` is also coprime with `z`. In mathematical terms, if there exist numbers `a` and `b` such that `a * x + b * z = 1`, and numbers `c` and `d` such that `c * y + d * z = 1`, then there must exist numbers `e` and `f` such that `e * (x * y) + f * z = 1`.
More concisely: If `x` and `z` are coprime, and `y` and `z` are coprime in a commutative semiring `R`, then `x * y` is coprime with `z`.
|
IsCoprime.add_mul_right_left
theorem IsCoprime.add_mul_right_left :
∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime (x + z * y) y
This theorem states that for any commutative ring `R`, if `x` and `y` are coprime elements in `R`, then for any other element `z` in `R`, `x + z*y` and `y` are also coprime. Here, two elements `x` and `y` are coprime if there exist two other elements `a` and `b` in `R` such that `a * x + b * y = 1`.
More concisely: If `x` and `y` are coprime elements in a commutative ring `R`, then `x` and `x + y * z` are coprime for any `z` in `R`.
|
IsCoprime.add_mul_left_left
theorem IsCoprime.add_mul_left_left :
∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime (x + y * z) y
This theorem states that for any commutative ring `R` and any elements `x`, `y`, and `z` of `R`, if `x` and `y` are coprime (meaning that there exist numbers `a` and `b` such that `a * x + b * y = 1`), then `x + y * z` and `y` are also coprime. In other words, if `x` and `y` share no common divisors other than 1, the same will hold true for the element `x + y * z` and `y`.
More concisely: If `x` and `y` are coprime elements in a commutative ring `R`, then `x` and `y + x * z` are coprime for all `z` in `R`.
|
IsRelPrime.neg_left
theorem IsRelPrime.neg_left : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → IsRelPrime (-x) y := by
sorry
This theorem states that for any type `R` that forms a commutative ring, and for any elements `x` and `y` of `R`, if `x` and `y` are relatively prime, then `-x` (the additive inverse of `x`) and `y` are also relatively prime. In plain English, if two numbers are relatively prime, then negating one of them doesn't change their relative primality.
More concisely: If `x` and `y` are relatively prime elements in a commutative ring `R`, then `-x` and `y` are also relatively prime.
|
isCoprime_one_left
theorem isCoprime_one_left : ∀ {R : Type u} [inst : CommSemiring R] {x : R}, IsCoprime 1 x
This theorem states that for any commutative semiring `R` and any element `x` of `R`, the number `1` and `x` are coprime. In the context of number theory, two numbers are said to be coprime if their greatest common divisor is `1`. This theorem formulates this concept in terms of the existence of coefficients `a` and `b` such that `a * 1 + b * x = 1`, which is always possible because `1` is the multiplicative identity in a semiring and thus, has no common divisors with any other element.
More concisely: For any commutative semiring `R` and its elements `1` and `x`, there exist coefficients `a, b ∈ R` such that `a * 1 + b * x = 1`.
|