primeSpectrum_asIdeal_range_eq — Mathlib

English

The range of the prime ideals' asIdeal map equals the range of the maximal ideals' asIdeal map.

Русский

Область значений отображения asIdeal для простых идеалов равна области значений отображения asIdeal для максимальных идеалов.

LaTeX

$$$\operatorname{range}(\text{PrimeSpectrum}.asIdeal) = \operatorname{range}(\text{MaximalSpectrum}.asIdeal)$$$

Lean4

theorem primeSpectrum_asIdeal_range_eq : range PrimeSpectrum.asIdeal = (range <| MaximalSpectrum.asIdeal (R := R)) := by
  simp only [PrimeSpectrum.range_asIdeal, MaximalSpectrum.range_asIdeal, isPrime_iff_isMaximal]

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