isIntegral_leadingCoeff_smul — Mathlib

English

Let p ∈ R[X] and x ∈ S with p.eval₂ f x = 0, where f: R →+* S. Then p.leadingCoeff · x is integral over R when viewed via the natural R-algebra structure.

Русский

Пусть p ∈ R[X] и x ∈ S удовлетворяют p.eval₂ f x = 0, где f: R →+* S. Тогда p.leadingCoeff · x интегрально над R во взаимном отношении.

LaTeX

$$$\bigl(p.eval_{f}(x)=0\bigr) \Rightarrow \ IsIntegral_R\bigl(p_{leadingCoeff} \cdot x\bigr)$$$

Lean4

/-- Given a `p : R[X]` and a root `x : S`,
then `p.leadingCoeff • x : S` is integral over `R`. -/
theorem isIntegral_leadingCoeff_smul [Algebra R S] (h : aeval x p = 0) : IsIntegral R (p.leadingCoeff • x) :=
  by
  rw [aeval_def] at h
  rw [Algebra.smul_def]
  exact (algebraMap R S).isIntegralElem_leadingCoeff_mul p x h

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