not_isField — Mathlib

English

For any commutative ring A, the power series ring A⟦X⟧ is not a field.

Русский

Для любого коммутативного кольца A кольцо степенных рядов A⟦X⟧ не является полем.

LaTeX

$$$\neg \mathrm{IsField}(\mathrm{PowerSeries}(A))$$$

Lean4

theorem not_isField : ¬IsField A⟦X⟧ := by
  by_cases hA : Subsingleton A
  · exact not_isField_of_subsingleton _
  · nontriviality A
    rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
    use Ideal.span { X }
    constructor
    · rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot]
      exact X_ne_zero
    · rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, Ideal.mem_span_singleton, X_dvd_iff, constantCoeff_one]
      exact one_ne_zero

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