English
For every nonzero prime P in A, the localized ring at P is not a field.
Русский
Для каждого ненулевого prime P в A локализация по P не является полем.
LaTeX
$$$\forall P [P.IsPrime], P ≠ ⊥ \Rightarrow ¬ IsField (Localization.AtPrime P)$$$
Lean4
theorem not_isField {P : Ideal A} (hP : P ≠ ⊥) [pP : P.IsPrime] (Aₘ : Type*) [CommRing Aₘ] [Algebra A Aₘ]
[IsLocalization.AtPrime Aₘ P] : ¬IsField Aₘ := by
intro h
letI := h.toField
obtain ⟨x, x_mem, x_ne⟩ := P.ne_bot_iff.mp hP
exact
(IsLocalRing.maximalIdeal.isMaximal _).ne_top
(Ideal.eq_top_of_isUnit_mem _ ((IsLocalization.AtPrime.to_map_mem_maximal_iff Aₘ P _).mpr x_mem)
(isUnit_iff_ne_zero.mpr
((map_ne_zero_iff (algebraMap A Aₘ) (IsLocalization.injective Aₘ P.primeCompl_le_nonZeroDivisors)).mpr x_ne)))
