instIsMaximalVanishingIdealSingletonForallSet

English

Over a field K that is algebraically closed and with a finite index σ, the vanishing ideal of a singleton {x} is a maximal ideal in MvPolynomial σ K.

Русский

Нулевой идеал синглтона {x} является максимальным идеалом в MvPolynomial σ K при K алгебраически замкнутом и конечном σ.

LaTeX

$$(vanishingIdeal K (\{x\})).IsMaximal$$

Lean4

instance {x : σ → K} : (vanishingIdeal K { x } : Ideal (MvPolynomial σ K)).IsMaximal :=
  by
  convert RingHom.ker_isMaximal_of_surjective (aeval (R := K) x) ?_
  · ext; simp
  · intro z; use C z; simp

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