instNontrivialAtPrime — Mathlib

English

The homogeneous localization at a prime is nontrivial; there exist distinct elements in the localized structure.

Русский

Однородная локализация по простому непустая; существуют различныe элементы в локализованной структуре.

LaTeX

$$$$ \mathrm{Nontrivial}(\mathrm{HomogeneousLocalization.AtPrime}(\mathcal{A}, \mathfrak{p})). $$$$

Lean4

instance : Nontrivial (HomogeneousLocalization.AtPrime 𝒜 𝔭) :=
  ⟨⟨0, 1, fun r => by simp [ext_iff_val, val_zero, val_one, zero_ne_one] at r⟩⟩

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