isMaximal — Mathlib

English

Let k be a field. In the multivariate polynomial ring over k in the variables Vars(k), the ideal maxIdeal k is a maximal ideal.

Русский

Пусть k — поле. В кольце многочленов над k в переменных Vars(k) идеал maxIdeal k является максимальным.

LaTeX

$$$\maxIdeal k \text{ is a maximal ideal of } \operatorname{MvPolynomial}(\mathrm{Vars}(k), k). $$$

Lean4

instance isMaximal : (maxIdeal k).IsMaximal :=
  (Classical.choose_spec <| Ideal.exists_le_maximal _ <| spanCoeffs_ne_top k).1

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