Polynomial.content_mul
theorem Polynomial.content_mul :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R] {p q : Polynomial R},
(p * q).content = p.content * q.content
The theorem `Polynomial.content_mul` states that for any commutative ring `R` that is also a domain and a normalized GCD monoid, and any two polynomials `p` and `q` with coefficients in `R`, the content (i.e., the greatest common divisor of the coefficients) of the polynomial resulting from multiplying `p` and `q` is equal to the product of the contents of `p` and `q`.
More concisely: For any commutative domain and normalized GCD monoid ring R, and polynomials p and q over R, the content of p q equals the product of the contents of p and q.
|
Polynomial.content_zero
theorem Polynomial.content_zero :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R],
Polynomial.content 0 = 0
The theorem `Polynomial.content_zero` states that for any type `R`, where `R` forms a commutative ring and is also a domain with a normalized greatest common divisor monoid structure, the `content` of the zero polynomial is zero. In other words, the greatest common divisor (gcd) of the coefficients of the zero polynomial is zero.
More concisely: In a commutative ring and domain with normalized greatest common divisors, the content of the zero polynomial is 0, meaning its coefficients have a gcd of 0.
|
Polynomial.isPrimitive_primPart
theorem Polynomial.isPrimitive_primPart :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R] (p : Polynomial R),
p.primPart.IsPrimitive
The theorem `Polynomial.isPrimitive_primPart` states that for any commutative ring `R` that is a domain and has a normalized greatest common divisor monoid, the primitive part of any polynomial `p` over `R` is a primitive polynomial. In other words, if a constant polynomial divides the primitive part of `p`, that constant polynomial is a unit. If `p` is the zero polynomial, its primitive part is taken to be 1, which is a primitive polynomial since the only constant polynomial (i.e., a scalar) dividing it is itself, which is a unit.
More concisely: For any commutative domain ring `R` with a normalized greatest common divisor monoid, the primitive part of a polynomial `p` over `R` is a primitive polynomial.
|
Polynomial.normalize_content
theorem Polynomial.normalize_content :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R] {p : Polynomial R},
normalize p.content = p.content
The theorem `Polynomial.normalize_content` states that for any commutative ring `R` which is also a domain and a normalized GCD monoid, and for any polynomial `p` with coefficients in `R`, the normalized content of the polynomial (i.e., the content obtained by multiplying the GCD of the coefficients by its normalization unit) is equal to its original content. In other words, normalization does not change the content of the polynomial.
More concisely: For any commutative domain and normalized GCD monoid ring R and polynomial p with coefficients in R, the normalized content of p equals its original content.
|
Polynomial.content_C
theorem Polynomial.content_C :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R] {r : R},
(Polynomial.C r).content = normalize r
This theorem states that for any commutative ring `R` which is also a domain and a normalized GCD monoid, and for any element `r` of `R`, the content of the constant polynomial `r` is equal to the normalization of `r`. In other words, the greatest common divisor (gcd) of the coefficients of the polynomial, which is simply `r` itself in this case, is equal to `r` multiplied by the norm unit of `r`. Here, the content function `Polynomial.content` computes the gcd of the coefficients of a polynomial, and the `normalize` function multiplies an element by its norm unit. The constant polynomial `r` is represented by `Polynomial.C r`, which is a ring homomorphism that takes an element of the ring and returns a constant polynomial with that element as the coefficient.
More concisely: For any commutative domain and normalized GCD monoid ring `R` and its element `r`, the content (greatest common divisor of coefficients) of the constant polynomial `r` equals the normalization of `r` (`r` multiplied by its norm unit).
|
Polynomial.isPrimitive_iff_content_eq_one
theorem Polynomial.isPrimitive_iff_content_eq_one :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R] {p : Polynomial R},
p.IsPrimitive ↔ p.content = 1
This theorem states that for any polynomial `p` over a type `R` (where `R` is a commutative ring, a domain, and a normalized GCD monoid), `p` is primitive if and only if the content of `p` is equal to one.
In more detail, a polynomial is primitive (as per the `Polynomial.IsPrimitive` definition) when the only constant polynomials that can divide it are units. The content of a polynomial (`Polynomial.content`) is defined as the greatest common divisor (GCD) of its coefficients. So, the theorem is saying that a polynomial has this property of being primitive if and only if the GCD of its coefficients is one.
More concisely: A polynomial over a commutative ring is primitive if and only if its content (greatest common divisor of coefficients) is equal to 1.
|
Polynomial.eq_C_content_mul_primPart
theorem Polynomial.eq_C_content_mul_primPart :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R] (p : Polynomial R),
p = Polynomial.C p.content * p.primPart
The theorem `Polynomial.eq_C_content_mul_primPart` states that for any polynomial `p` over a Commutative Ring `R` that also is a Domain and a Normalized GCD Monoid, `p` is equal to the product of a constant polynomial (whose constant is the greatest common divisor of the coefficients of `p`) and the primitive part of `p`. In essence, this theorem is expressing that any polynomial can be represented as a product of a constant polynomial and its primitive part.
More concisely: For any polynomial `p` over a commutative ring `R` that is a domain and a normalized GCD monoid, `p` equals the product of the constant polynomial with the greatest common divisor of its coefficients and the primitive part of `p`.
|
Polynomial.IsPrimitive.content_eq_one
theorem Polynomial.IsPrimitive.content_eq_one :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R] {p : Polynomial R},
p.IsPrimitive → p.content = 1
The theorem `Polynomial.IsPrimitive.content_eq_one` states that for any ring `R` which is a commutative ring, a domain, and has a normalized GCD monoid structure, if a polynomial `p` over `R` is primitive, then the content of `p` is equal to 1. Here, a polynomial is considered primitive if the only constant polynomials dividing it are units, and the content of a polynomial is defined as the greatest common divisor (GCD) of its coefficients.
More concisely: If `R` is a commutative ring, a domain, and has a normalized GCD monoid structure, and `p` is a primitive polynomial over `R`, then the content of `p` equals 1.
|
Polynomial.primPart_zero
theorem Polynomial.primPart_zero :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R],
Polynomial.primPart 0 = 1
This theorem states that for all types `R`, where `R` is a commutative ring, `R` forms a domain, and `R` is a normalized greatest common divisor monoid, the primitive part of the zero polynomial is equal to 1. In other words, when a polynomial is zero, its primitive part - the polynomial obtained by dividing the original polynomial by its content - is 1.
More concisely: For every commutative ring `R` that is a domain and a normalized greatest common divisor monoid, the primitive part of the zero polynomial is equal to the constant polynomial 1.
|
Polynomial.content_eq_zero_iff
theorem Polynomial.content_eq_zero_iff :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : NormalizedGCDMonoid R] {p : Polynomial R},
p.content = 0 ↔ p = 0
This theorem states that for any type `R` which is a commutative ring and a domain with a normalized greatest common divisor (GCD) monoid structure, and any polynomial `p` over `R`, the content of `p` (which is defined as the GCD of the coefficients of `p`) is equal to zero if and only if the polynomial `p` itself is the zero polynomial. In other words, a polynomial's content is zero precisely when the polynomial is the zero polynomial.
More concisely: For any commutative ring and domain `R` with a normalized greatest common divisor monoid structure, the content of a polynomial `p` over `R` is equal to zero if and only if `p` is the zero polynomial.
|