primeSpectrumEquivMaximalSpectrum_comp_asIdeal

English

The composition with asIdeal gives a map from prime spectrum to ideals matching maximal spectrum.

Русский

Композиция с asIdeal задаёт отображение от простого спектра к идеалам, согласованная с максимальным спектром.

LaTeX

$$$\mathrm{MaximalSpectrum.asIdeal} \circ \mathrm{primeSpectrumEquivMaximalSpectrum} = \mathrm{PrimeSpectrum.asIdeal} (R := R)$$$

Lean4

theorem primeSpectrumEquivMaximalSpectrum_comp_asIdeal :
    MaximalSpectrum.asIdeal ∘ primeSpectrumEquivMaximalSpectrum = PrimeSpectrum.asIdeal (R := R) :=
  rfl

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