IsBezout.span_gcd
theorem IsBezout.span_gcd :
∀ {R : Type u} [inst : Ring R] (x y : R) [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})],
Ideal.span {IsBezout.gcd x y} = Ideal.span {x, y}
The theorem `IsBezout.span_gcd` states that for any ring `R` and any two elements `x` and `y` of the ring, if the ideal generated by `x` and `y` is principal (i.e., it is generated by a single element), then the ideal generated by the greatest common divisor of `x` and `y` is the same as the ideal generated by `x` and `y`. This means that in the context of a Bézout domain (a ring in which every finitely generated ideal is principal), the greatest common divisor of two elements essentially captures the same information as the two original elements with respect to generating ideals.
More concisely: In a Bézout domain, the ideal generated by two elements is principal if and only if it is generated by their greatest common divisor.
|
IsBezout.gcd_dvd_right
theorem IsBezout.gcd_dvd_right :
∀ {R : Type u} [inst : CommRing R] (x y : R) [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})],
IsBezout.gcd x y ∣ y
The theorem `IsBezout.gcd_dvd_right` states that for any commutative ring `R` and any two elements `x` and `y` of `R`, if the ideal generated by `x` and `y` is principal (i.e., it can be generated by a single element), then the `gcd` of `x` and `y` (as defined in a Bézout domain) divides `y`. The Bézout domain is a particular kind of integral domain where every finitely generated ideal is principal, and a `gcd` in such a domain is not uniquely determined.
More concisely: In a commutative ring where every ideal is principal (a Bézout domain), the `gcd` of two elements `x` and `y` divides `y`.
|
Submodule.IsPrincipal.span_singleton_generator
theorem Submodule.IsPrincipal.span_singleton_generator :
∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Ring R] [inst_2 : Module R M] (S : Submodule R M)
[inst_3 : S.IsPrincipal], Submodule.span R {Submodule.IsPrincipal.generator S} = S
The theorem `Submodule.IsPrincipal.span_singleton_generator` states that for any ring `R`, any additively commutative group `M` and any `R`-module structure on `M`, and for any submodule `S` of `M` that is a principal submodule, the span of the set containing only the generator of `S` is equal to `S` itself. In other words, a principal submodule `S` is exactly the submodule spanned by its generator.
More concisely: A submodule of an `R`-module `M` is principal if and only if it is equal to the span of its generator.
|
IsRelPrime.isCoprime
theorem IsRelPrime.isCoprime :
∀ {R : Type u} [inst : CommRing R] {x y : R} [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})],
IsRelPrime x y → IsCoprime x y
The theorem `IsRelPrime.isCoprime` states that for any commutative ring `R` and any elements `x` and `y` of `R`, if the ideal generated by `x` and `y` is principal (i.e., can be generated by a single element), then if `x` and `y` are relatively prime (meaning any common divisor is a unit), it follows that `x` and `y` are coprime. In other words, there exist elements `a` and `b` in the ring such that `a * x + b * y = 1`. This theorem essentially connects the notions of relative primality and coprimality in the context of commutative rings with principal ideals.
More concisely: If `x` and `y` are relatively prime elements of a commutative ring `R` with principal ideal generated by `x` and `y`, then there exist `a` and `b` in `R` such that `a * x + b * y = 1`.
|
Ideal.span_singleton_generator
theorem Ideal.span_singleton_generator :
∀ {R : Type u} [inst : Ring R] (I : Ideal R) [inst_1 : Submodule.IsPrincipal I],
Ideal.span {Submodule.IsPrincipal.generator I} = I
The theorem `Ideal.span_singleton_generator` asserts that for any ring `R` and any ideal `I` of `R` that is a principal submodule, the ideal generated by the singleton set containing the generator of `I` is equal to `I` itself. In other words, if `I` is a principal ideal in `R` with generator `x`, then the ideal spanned by `{x}` is precisely `I`. This essentially states that a principal ideal in a ring is entirely determined by its generator.
More concisely: If `I` is a principal ideal in a ring `R` with generator `x`, then the ideal generated by `{x}` equals `I`.
|
gcd_isUnit_iff
theorem gcd_isUnit_iff :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsBezout R] [inst_3 : GCDMonoid R] (x y : R),
IsUnit (gcd x y) ↔ IsCoprime x y
This theorem states that for any commutative ring `R`, which is also a domain and a Bezout domain (i.e., a domain in which the greatest common divisor of any two elements can be expressed as a linear combination of those elements), and which additionally has a notion of a GCD monoid (a structure in which every two elements have a greatest common divisor), the greatest common divisor (gcd) of any two elements `x` and `y` in `R` is a unit (an element with a two-sided inverse) if and only if `x` and `y` are coprime. In other words, `x` and `y` are coprime - meaning there exist elements `a` and `b` in `R` such that `a * x + b * y = 1` - if and only if their gcd has a two-sided inverse in `R`.
More concisely: For a commutative domain `R` with a Bezout identity and GCD monoid, `x` and `y` in `R` are coprime if and only if the greatest common divisor of `x` and `y` is a unit in `R`.
|
PrincipalIdealRing.ringHom_mem_submonoid_of_factors_subset_of_units_subset
theorem PrincipalIdealRing.ringHom_mem_submonoid_of_factors_subset_of_units_subset :
∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
[inst_3 : Semiring S] (f : R →+* S) (s : Submonoid S) (a : R),
a ≠ 0 → (∀ b ∈ PrincipalIdealRing.factors a, f b ∈ s) → (∀ (c : Rˣ), f ↑c ∈ s) → f a ∈ s
The theorem `PrincipalIdealRing.ringHom_mem_submonoid_of_factors_subset_of_units_subset` states that for any `RingHom` (i.e., a ring homomorphism), denoted by `f`, from a commutative ring `R` to a semiring `S`, a submonoid `s` of `S`, and a non-zero element `a` of `R`, if `f` maps all irreducible factors of `a` (obtained by `PrincipalIdealRing.factors a`) and all units of `R` into `s`, then `f` also maps `a` itself into `s`. In essence, if a ring homomorphism preserves the irreducible factors and units under the mapping into a submonoid, then it also preserves the mapping of an element whose factors and units have been mapped.
More concisely: If a ring homomorphism maps all irreducible factors and units of a ring into a submonoid, then it maps any element whose factors and units belong to the submonoid into the submonoid as well.
|
IsPrincipalIdealRing.of_prime
theorem IsPrincipalIdealRing.of_prime :
∀ {R : Type u} [inst : CommRing R],
(∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P) → IsPrincipalIdealRing R
This theorem states that given any type `R` which is a commutative ring, if every prime ideal in `R` is a principal ideal (meaning it can be generated by a single element), then every other ideal in `R` is also a principal ideal. In other words, if all prime ideals in a commutative ring can be expressed as multiples of a single element, then this property extends to all ideals in the ring, making it a principal ideal ring.
More concisely: If every prime ideal in a commutative ring `R` is principal, then every ideal in `R` is principal.
|
IsBezout.isPrincipal_of_FG
theorem IsBezout.isPrincipal_of_FG :
∀ {R : Type u} [inst : Ring R] [self : IsBezout R] (I : Ideal R), I.FG → Submodule.IsPrincipal I
This theorem states that any finitely generated ideal in a ring `R` is principal, given that the ring `R` satisfies the Bezout identity property. Here, an ideal being 'finitely generated' means it can be generated by a finite number of elements. An ideal being 'principal' means it can be generated by a single element. The Bezout identity property for a ring refers to the existence of a linear combination of any two elements in the ring that equals their greatest common divisor. The theorem asserts that under these conditions, the finitely generated ideal is, in fact, a principal ideal.
More concisely: In a Bezout identity ring, every finitely generated ideal is principal.
|
Submodule.IsPrincipal.mem_iff_generator_dvd
theorem Submodule.IsPrincipal.mem_iff_generator_dvd :
∀ {R : Type u} [inst : CommRing R] (S : Ideal R) [inst_1 : Submodule.IsPrincipal S] {x : R},
x ∈ S ↔ Submodule.IsPrincipal.generator S ∣ x
This theorem is stating that for any commutative ring `R` and an ideal `S` of `R` that is principal, a given element `x` of `R` is in `S` if and only if the generator of `S` divides `x`. In other words, any element `x` is a member of a principal ideal `S` in the ring `R` exactly when it is a multiple of the generator of `S`. Here, a principal ideal is an ideal generated by a single element, and the generator of an ideal is that single element.
More concisely: A commutative ring's ideal is principal and generated by x if and only if x divisibly covers all elements in the ideal.
|
Irreducible.coprime_iff_not_dvd
theorem Irreducible.coprime_iff_not_dvd :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsBezout R] {p n : R}, Irreducible p → (IsCoprime p n ↔ ¬p ∣ n) := by
sorry
This theorem states that, for any commutative ring `R` with a Bezout identity and any elements `p` and `n` of `R`, if `p` is irreducible, then `p` and `n` are coprime (i.e., there exist `a` and `b` in `R` such that `a * p + b * n = 1`) if and only if `p` does not divide `n`. In other words, an irreducible element `p` is coprime with `n` precisely when it is not a divisor of `n`.
More concisely: An irreducible element in a commutative ring with a Bezout identity is coprime with another element if and only if it doesn't divide that element.
|
nonPrincipals_zorn
theorem nonPrincipals_zorn :
∀ {R : Type u} [inst : CommRing R],
∀ c ⊆ nonPrincipals R,
IsChain (fun x x_1 => x ≤ x_1) c → ∀ {K : Ideal R}, K ∈ c → ∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I
The theorem `nonPrincipals_zorn` states that for any given type `R` with a commutative ring structure, every chain within the set of non-principal ideals of `R` has an upper bound that is also a non-principal ideal. A chain is defined as a set where, for any two elements, one is less than the other, or they are equal. The chain is a subset of the non-principal ideals, and the theorem further states that for any ideal `K` in the chain, there exists a non-principal ideal `I` such that every ideal `J` in the chain is less than or equal to `I`. The upper bound is provided by the union of the elements in the chain.
More concisely: Every chain of non-principal ideals in a commutative ring has a supremum, which is a non-principal ideal.
|
IsBezout.gcd_dvd_left
theorem IsBezout.gcd_dvd_left :
∀ {R : Type u} [inst : CommRing R] (x y : R) [inst_1 : Submodule.IsPrincipal (Ideal.span {x, y})],
IsBezout.gcd x y ∣ x
The theorem `IsBezout.gcd_dvd_left` states that for any commutative ring `R` and any two elements `x` and `y` of `R`, if the ideal generated by `x` and `y` is principal (i.e., it can be generated by a single element), then the greatest common divisor (`gcd`) of `x` and `y` (as defined in a Bézout domain) divides `x`. In other words, `x` is a multiple of the `gcd` of `x` and `y`.
More concisely: In a commutative ring, if the ideal generated by two elements is principal, then the greatest common divisor of those elements divides one of them.
|
Submodule.IsPrincipal.generator_mem
theorem Submodule.IsPrincipal.generator_mem :
∀ {R : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : Ring R] [inst_2 : Module R M] (S : Submodule R M)
[inst_3 : S.IsPrincipal], Submodule.IsPrincipal.generator S ∈ S
The theorem `Submodule.IsPrincipal.generator_mem` asserts that, for any given type `R` which is a ring and type `M` which is an additive commutative group and a module over `R`, if you have a submodule `S` of `M` which is a principal submodule, then the generator of `S` (that is, an element `x` in `M` such that `S` is the span of `{x}`) is itself an element of the submodule `S`. This theorem is essentially stating that the generator of a principal submodule is always a member of that submodule.
More concisely: If `S` is a principal submodule of the `R`-module `M`, then the generator of `S` is an element of `S`.
|
IsPrincipalIdealRing.of_surjective
theorem IsPrincipalIdealRing.of_surjective :
∀ {R : Type u} {S : Type u_1} [inst : Ring R] [inst_1 : Ring S] [inst_2 : IsPrincipalIdealRing R] (f : R →+* S),
Function.Surjective ⇑f → IsPrincipalIdealRing S
The theorem `IsPrincipalIdealRing.of_surjective` states that for any two Types `R` and `S`, given that `R` is a ring, `S` is also a ring, and `R` is a principal ideal ring, if there exists a ring homomorphism `f` from `R` to `S` that is surjective (i.e., for every element in `S`, there is at least one element in `R` that maps to it via `f`), then `S` is also a principal ideal ring.
More concisely: If `R` is a principal ideal ring and `f` is a surjective ring homomorphism from `R` to `S`, then `S` is a principal ideal ring.
|
exists_gcd_eq_mul_add_mul
theorem exists_gcd_eq_mul_add_mul :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsBezout R] [inst_3 : GCDMonoid R] (a b : R),
∃ x y, gcd a b = a * x + b * y
**Bézout's Lemma**: This theorem states that for any type `R` which is a Commutative Ring, a Domain, has a Bézout identity, and a Greatest Common Divisor (GCD) Monoid, and for any two values `a` and `b` of type `R`, there exist `x` and `y` such that the GCD of `a` and `b` can be expressed as a linear combination of `a` and `b`. In other words, the GCD of `a` and `b` equals `a` multiplied by `x` plus `b` multiplied by `y`.
More concisely: For any commutative ring `R` that is a domain, has a Bezout identity, and a greatest common divisor monoid, there exist integers `x` and `y` such that the greatest common divisor of elements `a` and `b` in `R` equals `a` multiplied by `x` plus `b` multiplied by `y`.
|
PrincipalIdealRing.isMaximal_of_irreducible
theorem PrincipalIdealRing.isMaximal_of_irreducible :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsPrincipalIdealRing R] {p : R},
Irreducible p → Ideal.IsMaximal (Submodule.span R {p})
This theorem states that in any Principal Ideal Ring `R`, which is a commutative ring where every ideal is principal, if `p` is an irreducible element of `R`, then the ideal generated by `p` (that is, the smallest submodule of `R` that contains `p`, denoted by `Submodule.span R {p}`) is a maximal ideal. An irreducible element is an element that cannot be expressed as the product of two other non-unit elements, and a maximal ideal is an ideal that is as large as possible without being equal to the whole ring.
More concisely: In a commutative Principal Ideal Ring `R`, an irreducible element `p` generates a maximal ideal.
|