not_isField — Mathlib

English

The ring of integers 𝓞_K is not a field.

Русский

Кольцо целых 𝓞_K не является полем.

LaTeX

$$$\\mathcal{O}_K \\text{ is not a field}$$$

Lean4

/-- The ring of integers of a number field is not a field. -/
theorem not_isField : ¬IsField (𝓞 K) :=
  by
  have h_inj : Function.Injective (algebraMap ℤ (𝓞 K)) := RingHom.injective_int (algebraMap ℤ (𝓞 K))
  intro hf
  exact Int.not_isField (((IsIntegralClosure.isIntegral_algebra ℤ K).isField_iff_isField h_inj).mpr hf)

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