isField_iff_maximalIdeal_eq — Mathlib

English

A local ring R is a field if and only if its maximal ideal is zero.

Русский

Локальное кольцо R является полем тогда и только тогда, когда его максимальный идеал равен нулю.

LaTeX

$$$ \text{IsField}(R) \iff \ maximalIdeal(R) = \{0\}. $$$

Lean4

theorem isField_iff_maximalIdeal_eq : IsField R ↔ maximalIdeal R = ⊥ :=
  not_iff_not.mp
    ⟨Ring.ne_bot_of_isMaximal_of_not_isField inferInstance, fun h =>
      Ring.not_isField_iff_exists_prime.mpr ⟨_, h, Ideal.IsMaximal.isPrime' _⟩⟩

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