Theorems · Theorem · commutative algebra

num_dvd_of_is_root

• 1000+ list: Rational root theorem

∀ {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

Rational root theorem part 1: if r : f.codomain is a root of a polynomial over the ufd A, then the numerator of r divides the constant coefficient

Defined in

Mathlib.RingTheory.Polynomial.RationalRoot

Cited by

1 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDomainUniqueFactorizationMonoidFieldAlgebraIsFractionRing