exists_dvd_map_of_isAlgebraic — Mathlib

English

For any σ and f ∈ MvPolynomial σ S with f ≠ 0 algebraic over R, there exists g ∈ MvPolynomial σ R with g ≠ 0 and f | g.map(algebraMap R S).

Русский

Для любого σ и f ∈ MvPolynomial σ S с f ≠ 0 и алгебраическим над R существует g ∈ MvPolynomial σ R, g ≠ 0, и f делится наg.map(алгебраическая карта R → S).

LaTeX

$$$\exists g \in MvPolynomial\,σ\,R,\ g \neq 0 \land f \mid g.map(\text{algebraMap }R S)$$$

Lean4

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

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