num_dvd_of_is_root — Mathlib

English

Let p be a monic polynomial over a UFD A. If r in the fraction field is a root of p, then there exists r' in A such that r = algebraMap_A_K(r') and r' divides the constant term p.coeff 0.

Русский

Пусть p — моноичный полином над UFD A. Если r в поле дробей является корнем p, то найдётся r' ∈ A such that r = алгебраическое отображение r' в K и r' делит константный коэффициент p.coeff 0.

LaTeX

$$$\\exists r'\\in A,\\; r = \\ algebraMap A K\\, r' \\;\u2217\\; r' \\mid p(0)$$$

Lean4

/-- **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 -/
theorem num_dvd_of_is_root {p : A[X]} {r : K} (hr : aeval r p = 0) : num A r ∣ p.coeff 0 :=
  by
  suffices num A r ∣ (scaleRoots p (den A r)).coeff 0
    by
    simp only [coeff_scaleRoots, tsub_zero] at this
    haveI inst := Classical.propDecidable
    by_cases hr : num A r = 0
    · simp_all [nonZeroDivisors.coe_ne_zero]
    · refine dvd_of_dvd_mul_left_of_no_prime_factors hr ?_ this
      intro q dvd_num dvd_denom_pow hq
      apply hq.not_unit
      exact num_den_reduced A r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow)
  convert dvd_term_of_isRoot_of_dvd_terms 0 (num_isRoot_scaleRoots_of_aeval_eq_zero hr) _
  · rw [pow_zero, mul_one]
  intro j hj
  apply dvd_mul_of_dvd_right
  convert pow_dvd_pow (num A r) (Nat.succ_le_of_lt (bot_lt_iff_ne_bot.mpr hj))
  exact (pow_one _).symm

Похожие утверждения