den_dvd_of_is_root
theorem den_dvd_of_is_root :
∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A]
[inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {p : Polynomial A} {r : K},
(Polynomial.aeval r) p = 0 → ↑(IsFractionRing.den A r) ∣ p.leadingCoeff
The theorem `den_dvd_of_is_root` is a statement of a part of the Rational Root Theorem. It states that for any commutative ring `A` which is a unique factorization domain, its field of fractions `K`, a polynomial `p` with coefficients in `A`, and a root `r` of `p` in `K`, if `r` is a root of the polynomial (i.e., its evaluation at `r` is zero), then the denominator of `r` (when expressed as a reduced fraction in the field of fractions `K`) divides the leading coefficient of the polynomial `p`.
More concisely: In a commutative unique factorization domain `A`, if a polynomial `p` in `A` has a root `r` in its field of fractions `K`, then the denominator of `r` divides the leading coefficient of `p`.
|
isInteger_of_is_root_of_monic
theorem isInteger_of_is_root_of_monic :
∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A]
[inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {p : Polynomial A},
p.Monic → ∀ {r : K}, (Polynomial.aeval r) p = 0 → IsLocalization.IsInteger A r
The theorem, "Integral Root Theorem", states that if `r` (a value in the field `K`, which is the field of fractions of an integral domain `A`) is a root of a monic polynomial (a polynomial with coefficient 1 on its highest degree term) over the unique factorization domain `A`, then `r` is an integer. In other words, if a monic polynomial evaluated at `r` gives zero, then `r` is in the image of the localization map from `A` to `K`. This theorem is important in number theory and algebra, as it provides a condition under which we can assert that a root of a polynomial is an integer.
More concisely: If a monic polynomial over a unique factorization domain has a root in its field of fractions, then that root is an integer.
|
num_dvd_of_is_root
theorem num_dvd_of_is_root :
∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A]
[inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {p : Polynomial A} {r : K},
(Polynomial.aeval r) p = 0 → IsFractionRing.num A r ∣ p.coeff 0
The **Rational Root Theorem part 1** is a theorem in the field of algebra. It states that, given an integral domain `A` which is a Unique Factorization Monoid and a field `K` which is the field of fractions of `A`, if `r` from `K` (meaning, `r` is a fraction) is a root of a polynomial `p` with coefficients in `A`, then the numerator of `r` divides the constant coefficient of the polynomial `p`. In other words, if a fraction is a root of a polynomial, then the fraction's numerator divides the constant term of the polynomial.
More concisely: If a rational number `r` is a root of a polynomial `p` with integral domain coefficients `A`, then the numerator of `r` divides the constant coefficient of `p`.
|