instIsAlgebraicPolynomialOfNoZeroDivisors_1

English

If [NoZeroDivisors S] and R ⟶ S is algebraic, then the polynomial ring R[X] is algebraic over S[X]; the algebraicity is preserved by adjoining indeterminates.

Русский

Если S без нулевых делителей, и R ⟶ S алгебраично, то полиномиальные кольца R[X] и S[X] образуют алгебраическое расширение, т.е. алгебраичность сохраняется при добавлении переменной X.

LaTeX

$$$[NoZeroDivisors S] \Rightarrow Algebra.IsAlgebraic\, (R[X])\,(S[X])$$$

Lean4

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

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