X_prime — Mathlib

English

The indeterminate X is a prime element of the ring R[[X]] over a domain R.

Русский

Индетерминант X является простым элементом кольца R[[X]] над доменом R.

LaTeX

$$X is a prime element of R[[X]]$$

Lean4

/-- The variable of the power series ring over an integral domain is prime. -/
theorem X_prime : Prime (X : R⟦X⟧) := by
  rw [← Ideal.span_singleton_prime]
  · exact span_X_isPrime
  · intro h
    simpa [map_zero (coeff 1)] using congr_arg (coeff 1) h

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