exists_dvd_map_of_isAlgebraic — Mathlib

English

Let f ∈ S[X] be nonzero and algebraic over R via the inclusion R → S. Then there exists g ∈ R[X], g ≠ 0 such that f divides g mapped to S[X] via the algebra map R → S.

Русский

Пусть f ∈ S[X] ненулевой и алгебраически над R через включение R → S. Тогда существует g ∈ R[X], g ≠ 0, такой что f делится наg, отображённое в S[X] через алгебраическое отображение R → S.

LaTeX

$$$\exists g \in R[X],\ g \neq 0 \ \land\ f \mid g^{\uparrow}$, где $g^{\uparrow}$ — образ g в S[X] по $R \to S$$$

Lean4

theorem exists_dvd_map_of_isAlgebraic [NoZeroDivisors S] {f : S[X]} (hf : f ≠ 0) :
    ∃ g : R[X], g ≠ 0 ∧ f ∣ g.map (algebraMap R S) :=
  (Algebra.IsAlgebraic.isAlgebraic f).exists_nonzero_dvd (mem_nonZeroDivisors_of_ne_zero hf)

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