toPrimeSpectrum_injective — Mathlib

English

The natural map from the maximal spectrum to the prime spectrum is injective.

Русский

Естественное отображение из максимального спектра в спектр простых инъективно.

LaTeX

$$$\mathrm{toPrimeSpectrum}: \mathrm{MaximalSpectrum}(R) \to \mathrm{PrimeSpectrum}(R)$ is injective$$

Lean4

theorem toPrimeSpectrum_injective : (@toPrimeSpectrum R _).Injective := fun ⟨_, _⟩ ⟨_, _⟩ h => by
  simpa only [MaximalSpectrum.mk.injEq] using PrimeSpectrum.ext_iff.mp h

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