primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal

English

The composition with the inverse equivalence yields the corresponding relation on ideals.

Русский

Композиция с обратной эквивалентностью даёт соответствие между идеалами.

LaTeX

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

Lean4

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

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