instIsAlgebraicMvPolynomialOfNoZeroDivisors

English

For any σ and nonzero f ∈ MvPolynomial σ S that is algebraic over R, there exists g ∈ MvPolynomial σ R, g ≠ 0, such that f divides g.map(algebraMap R S).

Русский

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

LaTeX

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

Lean4

instance {σ} [NoZeroDivisors R] : Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S) :=
  Algebra.IsPushout.isAlgebraic R S ..

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