Commit 2023-05-25 08:46 6994f45f

View on Github →

feat: port AlgebraicGeometry.PrimeSpectrum.Maximal (#4323)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicGeometry/PrimeSpectrum/Maximal.lean

added theorem MaximalSpectrum.iInf_localization_eq_bot

added def MaximalSpectrum.toPrimeSpectrum

added theorem MaximalSpectrum.toPrimeSpectrum_continuous

added theorem MaximalSpectrum.toPrimeSpectrum_injective

added theorem MaximalSpectrum.toPrimeSpectrum_range

added structure MaximalSpectrum

added theorem PrimeSpectrum.iInf_localization_eq_bot