maxIdeal — Mathlib

English

There exists a maximal ideal M of the polynomial ring containing spanCoeffs(k). This ideal is obtained by a choice from Ideal.exists_le_maximal applied to spanCoeffs_ne_top.

Русский

Существует максимальный идеал M кольца многочленов, содержащий spanCoeffs(k). Этот идеал получается с помощью выбора из Ideal.exists_le_maximal при spanCoeffs_ne_top.

LaTeX

$$maxIdeal(k) = \\text{the maximal ideal containing spanCoeffs}(k)$$

Lean4

/-- A random maximal ideal that contains `spanEval k` -/
def maxIdeal : Ideal (MvPolynomial (Vars k) k) :=
  Classical.choose <| Ideal.exists_le_maximal _ <| spanCoeffs_ne_top k

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