num_isRoot_scaleRoots_of_aeval_eq_zero

English

If a polynomial p has a root x in a fraction field K of A, then the polynomial scaleRoots(p, den A x) has root num A x.

Русский

Если p имеет корень x в поле дробей K, то scaleRoots(p, den A x) имеет корень num A x.

LaTeX

$$$\\text{If } \\mathrm{aeval}\\, x\\, p = 0, \\text{ then } \\text{IsRoot}(\\mathrm{scaleRoots}(p, \\mathrm{den} A x), \\mathrm{num} A x).$$$

Lean4

theorem num_isRoot_scaleRoots_of_aeval_eq_zero [UniqueFactorizationMonoid A] {p : A[X]} {x : K} (hr : aeval x p = 0) :
    IsRoot (scaleRoots p (den A x)) (num A x) :=
  by
  apply isRoot_of_eval₂_map_eq_zero (IsFractionRing.injective A K)
  refine scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero ?_
  rw [mk'_num_den]
  exact hr

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