span_X_isPrime — Mathlib

English

In a polynomial or power series ring over a domain, the ideal generated by X is prime.

Русский

В кольце над доменом идеал, порождаемый X, является простым.

LaTeX

$$(X) is a prime ideal in k[[X]] (or R[[X]]).$$

Lean4

/-- The ideal spanned by the variable in the power series ring
over an integral domain is a prime ideal. -/
theorem span_X_isPrime : (Ideal.span ({ X } : Set R⟦X⟧)).IsPrime :=
  by
  suffices Ideal.span ({ X } : Set R⟦X⟧) = RingHom.ker constantCoeff
    by
    rw [this]
    exact RingHom.ker_isPrime _
  apply Ideal.ext
  intro φ
  rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]

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