instIsAlgebraicMvPolynomialOfNoZeroDivisors_1

English

If R has NoZeroDivisors, then Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S) holds whenever Algebra.IsAlgebraic R S holds.

Русский

Если у R нет нулевых делителей, то Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S) сохраняется при условии Algebra.IsAlgebraic R S.

LaTeX

$$$[NoZeroDivisors\;R] \Rightarrow Algebra.IsAlgebraic(\,MvPolynomial\;σ\;R)(MvPolynomial\;σ\;S)$$$

Lean4

instance {σ} [NoZeroDivisors S] : Algebra.IsAlgebraic (MvPolynomial σ R) (MvPolynomial σ S) :=
  by
  by_cases h : Function.Injective (algebraMap R S)
  · have := h.noZeroDivisors _ (map_zero _) (map_mul _); infer_instance
  rw [← MvPolynomial.map_injective_iff] at h
  exact Algebra.isAlgebraic_of_not_injective h

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