nontrivial — Mathlib

English

The localization at the complement of a prime ideal P is a nontrivial local ring; in particular, it is a local ring.

Русский

Локализация по дополнению к простому идеалу P является ненулевым локальным кольцом; в частности, это локальное кольцо.

LaTeX

$$$$ \text{IsLocalRing}( Localization.P.primeCompl ) $$$$

Lean4

theorem nontrivial [IsLocalization.AtPrime S P] : Nontrivial S :=
  nontrivial_of_ne (0 : S) 1 fun hze =>
    by
    rw [← (algebraMap R S).map_one, ← (algebraMap R S).map_zero] at hze
    obtain ⟨t, ht⟩ := (eq_iff_exists P.primeCompl S).1 hze
    have htz : (t : R) = 0 := by simpa using ht.symm
    exact t.2 (htz.symm ▸ P.zero_mem : ↑t ∈ P)

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