instIsPrimeVanishingIdealSingletonForallSet

English

The vanishing ideal of a singleton {x} is a prime ideal in the polynomial ring MvPolynomial σ k.

Русский

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

LaTeX

$$$(\operatorname{vanishingIdeal}(k, \{x\}) : \operatorname{Ideal}(\operatorname{MvPolynomial}(\sigma, k))).IsPrime$$$

Lean4

instance {x : σ → K} : (vanishingIdeal k { x } : Ideal (MvPolynomial σ k)).IsPrime :=
  by
  convert RingHom.ker_isPrime (aeval (R := k) x)
  ext; simp

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