Topology

📁 Source: Mathlib/RingTheory/Spectrum/Prime/Topology.lean

Statistics

Metric	Count
Definitions equivIrreducibleComponents, closedPoint, instBoundedOrderPrimeSpectrumOfIsDomain, instOrderTopPrimeSpectrum, toPiLocalizationEquiv, basicOpen, closedsEmbedding, homeomorphOfRingEquiv, isIdempotentElemEquivClopens, localizationMapOfSpecializes, mulZeroAddOneEquivClopens, nhdsOrderEmbedding, pointsEquivIrreducibleCloseds, primeSpectrumProdHomeo, zariskiTopology, zeroLocusEquivIrreducibleCloseds, equivIrreducibleComponents	17
Theorems asIdeal_top, comap_residue, eq_bot_or_eq_top, closedPoint_mem_iff, closed_point_mem_iff, comap_closedPoint, isClosed_singleton_closedPoint, isLocalHom_iff_comap_closedPoint, specializes_closedPoint, basicOpen_eq_bot_iff, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_of_isIdempotentElem, basicOpen_eq_zeroLocus_of_mul_add, basicOpen_injOn_isIdempotentElem, basicOpen_isIdempotentElemEquivClopens_symm, basicOpen_le_basicOpen_iff, basicOpen_le_basicOpen_iff_algebraMap_isUnit, basicOpen_mul, basicOpen_mul_le_left, basicOpen_mul_le_right, basicOpen_one, basicOpen_pow, basicOpen_zero, closure_image_comap_zeroLocus, closure_range_comap, closure_singleton, coe_isIdempotentElemEquivClopens_apply, comap_apply, comap_basicOpen, comap_isInducing_of_surjective, comap_quotientMk_bijective_of_le_nilradical, comap_singleton_isClosed_of_surjective, compactSpace, continuous_comap, denseRange_comap_iff_ker_le_nilRadical, denseRange_comap_iff_minimalPrimes, discreteTopology_iff_finite_and_krullDimLE_zero, discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, discreteTopology_iff_toPiLocalization_bijective, discreteTopology_iff_toPiLocalization_surjective, discreteTopology_of_toLocalization_surjective, eq_biUnion_of_isOpen, existsUnique_idempotent_basicOpen_eq_of_isClopen, exists_idempotent_basicOpen_eq_of_isClopen, exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen, iSup_basicOpen_eq_top_iff, iSup_basicOpen_eq_top_iff', instPrespectralSpace, instQuasiSeparatedSpace, instQuasiSoberElemZeroLocus, instSpectralSpace, instT0Space, irreducibleSpace, isBasis_basic_opens, isClopen_basicOpen_of_mul_add, isClopen_iff, isClopen_iff_mul_add, isClopen_iff_mul_add_zeroLocus, isClopen_iff_zeroLocus, isClosedEmbedding_comap_fst, isClosedEmbedding_comap_of_surjective, isClosedEmbedding_comap_snd, isClosedMap_comap_of_isIntegral, isClosed_comap_singleton_of_isIntegral, isClosed_iff_zeroLocus, isClosed_iff_zeroLocus_ideal, isClosed_iff_zeroLocus_radical_ideal, isClosed_image_of_stableUnderSpecialization, isClosed_range_comap_of_surjective, isClosed_range_of_stableUnderSpecialization, isClosed_singleton_iff_isMaximal, isClosed_zeroLocus, isCompact_basicOpen, isCompact_isOpen_iff, isCompact_isOpen_iff_ideal, isConstructible_basicOpen, isEmbedding_comap_of_surjective, isHomeomorph_comap_of_bijective, isIdempotentElemEquivClopens_apply_toOpens, isIdempotentElemEquivClopens_mul, isIdempotentElemEquivClopens_one_sub, isIdempotentElemEquivClopens_symm_bot, isIdempotentElemEquivClopens_symm_compl, isIdempotentElemEquivClopens_symm_inf, isIdempotentElemEquivClopens_symm_sup, isIdempotentElemEquivClopens_symm_top, isIntegral_of_isClosedMap_comap_mapRingHom, isIrreducible_iff_vanishingIdeal_isPrime, isIrreducible_zeroLocus_iff, isIrreducible_zeroLocus_iff_of_radical, isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton, isOpen_basicOpen, isOpen_iff, isQuotientMap_of_generalizingMap, isQuotientMap_of_specializingMap, isRadical_vanishingIdeal, isRetrocompact_basicOpen, isRetrocompact_zeroLocus_compl, isRetrocompact_zeroLocus_compl_of_fg, isTopologicalBasis_basic_opens, le_basicOpen_pow, le_iff_mem_closure, le_iff_specializes, localization_away_comap_range, localization_away_isOpenEmbedding, localization_comap_injective, localization_comap_isEmbedding, localization_comap_isInducing, localization_comap_range, localization_specComap_injective, localization_specComap_range, maximalSpectrumToPiLocalization_surjective_of_discreteTopology, mem_basicOpen, nhdsOrderEmbedding_apply, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr, quasiSober, range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, range_comap_fst, range_comap_snd, stableUnderGeneralization_singleton, stableUnderSpecialization_image_iff, stableUnderSpecialization_range_iff, stableUnderSpecialization_singleton, t1Space_iff_isField, toPiLocalization_bijective, toPiLocalization_surjective_of_discreteTopology, topologicalKrullDim_eq_ringKrullDim, vanishingIdeal_anti_mono_iff, vanishingIdeal_closure, vanishingIdeal_irreducibleComponents, vanishingIdeal_isClosed_isIrreducible, vanishingIdeal_isIrreducible, vanishingIdeal_mem_minimalPrimes, vanishingIdeal_range_comap, vanishingIdeal_strict_anti_mono_iff, zeroLocus_eq_basicOpen_of_isIdempotentElem, zeroLocus_eq_basicOpen_of_mul_add, zeroLocus_eq_iff, zeroLocus_ideal_mem_irreducibleComponents, zeroLocus_minimalPrimes, zeroLocus_vanishingIdeal_eq_closure, comap_surjective, specComap_surjective	144
Total	161

Ideal.minimalPrimes

Definitions

Name	Category	Theorems
equivIrreducibleComponents 📖	CompOp	—

IsLocalRing

Definitions

Name	Category	Theorems
closedPoint 📖	CompOp	37 math math: AlgebraicGeometry.Scheme.toSpecΓ_apply, AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, closedPoint_mem_iff, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_closedPoint, isClosed_singleton_closedPoint, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_snd_coe, comap_closedPoint, AlgebraicGeometry.pointEquivClosedPoint_apply_coe, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.Scheme.stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.germ_stalkClosedPointIso_hom_assoc, specializes_closedPoint, closedPoint_mem_support, PrimeSpectrum.comap_residue, AlgebraicGeometry.germ_stalkClosedPointIso_hom, AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst, closed_point_mem_iff, AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv, AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo', AlgebraicGeometry.IsAffineOpen.primeIdealOf_eq_map_closedPoint, isLocalHom_iff_comap_closedPoint, AlgebraicGeometry.Scheme.SpecMap_residue_apply, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply, AlgebraicGeometry.Spec_closedPoint, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_base_apply, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.Scheme.germ_stalkClosedPointTo_Spec, AlgebraicGeometry.stalkClosedPointIso_inv, AlgebraicGeometry.Scheme.isLocalHom_stalkClosedPointTo, AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField_apply, AlgebraicGeometry.Scheme.stalkClosedPointTo_comp, AlgebraicGeometry.Scheme.Spec_map_residue_apply, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk, AlgebraicGeometry.Spec_stalkClosedPointIso, AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, AlgebraicGeometry.Scheme.toSpecΓ_base
instBoundedOrderPrimeSpectrumOfIsDomain 📖	CompOp	—
instOrderTopPrimeSpectrum 📖	CompOp	2 math math: PrimeSpectrum.asIdeal_top, Ring.KrullDimLE.eq_bot_or_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedPoint_mem_iff 📖	mathematical	—	PrimeSpectrum TopologicalSpace.Opens PrimeSpectrum.zariskiTopology SetLike.instMembership TopologicalSpace.Opens.instSetLike closedPoint Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff Specializes.mem_open specializes_closedPoint TopologicalSpace.Opens.is_open' TopologicalSpace.Opens.mem_top
closed_point_mem_iff 📖	mathematical	—	PrimeSpectrum TopologicalSpace.Opens PrimeSpectrum.zariskiTopology SetLike.instMembership TopologicalSpace.Opens.instSetLike closedPoint Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	eq_top_iff Specializes.mem_open specializes_closedPoint TopologicalSpace.Opens.is_open'
comap_closedPoint 📖	mathematical	—	PrimeSpectrum.comap closedPoint	—	isLocalHom_iff_comap_closedPoint
isClosed_singleton_closedPoint 📖	mathematical	—	IsClosed PrimeSpectrum PrimeSpectrum.zariskiTopology Set Set.instSingletonSet closedPoint	—	PrimeSpectrum.isClosed_singleton_iff_isMaximal closedPoint.eq_1 maximalIdeal.isMaximal
isLocalHom_iff_comap_closedPoint 📖	mathematical	—	IsLocalHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike PrimeSpectrum.comap closedPoint	—	RingHom.instRingHomClass List.TFAE.out local_hom_TFAE PrimeSpectrum.ext_iff
specializes_closedPoint 📖	mathematical	—	Specializes PrimeSpectrum PrimeSpectrum.zariskiTopology closedPoint	—	PrimeSpectrum.le_iff_specializes le_maximalIdeal Ideal.IsPrime.ne_top' PrimeSpectrum.isPrime

IsLocalRing.PrimeSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asIdeal_top 📖	mathematical	—	PrimeSpectrum.asIdeal Top.top PrimeSpectrum OrderTop.toTop Preorder.toLE PartialOrder.toPreorder PrimeSpectrum.instPartialOrder IsLocalRing.instOrderTopPrimeSpectrum IsLocalRing.maximalIdeal	—	—
comap_residue 📖	mathematical	—	PrimeSpectrum.comap IsLocalRing.ResidueField CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield IsLocalRing.ResidueField.field IsLocalRing.residue IsLocalRing.closedPoint	—	instIsDomain Unique.instSubsingleton PrimeSpectrum.ext Ideal.mk_ker

IsLocalRing.Ring.KrullDimLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_bot_or_eq_top 📖	mathematical	—	Bot.bot PrimeSpectrum OrderBot.toBot Preorder.toLE PartialOrder.toPreorder PrimeSpectrum.instPartialOrder PrimeSpectrum.instOrderBotOfIsDomain Top.top OrderTop.toTop IsLocalRing.instOrderTopPrimeSpectrum	—	Order.krullDim_le_one_iff_of_boundedOrder Order.KrullDimLE.krullDim_le

MaximalSpectrum

Definitions

Name	Category	Theorems
toPiLocalizationEquiv 📖	CompOp	—

PrimeSpectrum

Definitions

Name	Category	Theorems
basicOpen 📖	CompOp	89 math math: basicOpen_pow, AlgebraicGeometry.Scheme.map_PrimeSpectrum_basicOpen_of_affine, isClopen_iff_mul_add, Polynomial.mem_image_comap_C_basicOpen, LocalizedModule.subsingleton_iff_disjoint, eq_biUnion_of_isOpen, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_preimage_basicOpen, basicOpen_injOn_isIdempotentElem, MvPolynomial.image_comap_C_basicOpen, AlgebraicGeometry.SpecMap_preimage_basicOpen, Algebra.basicOpen_subset_etaleLocus_iff_etale, basicOpen_eq_zeroLocus_of_mul_add, AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, Module.basicOpen_subset_freeLocus_iff, AlgebraicGeometry.StructureSheaf.exists_const, Algebra.basicOpen_subset_unramifiedLocus_iff, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpenPowersToOpenₗ, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_eq, AlgebraicGeometry.StructureSheaf.to_basicOpen_epi, le_basicOpen_pow, iSup_basicOpen_eq_top_iff, isConstructible_basicOpen, basicOpen_mul, basicOpen_eq_zeroLocus_of_isIdempotentElem, zeroLocus_eq_basicOpen_of_isIdempotentElem, AlgebraicGeometry.IsAffineOpen.basicOpen_fromSpec_app, basicOpen_le_basicOpen_iff_algebraMap_isUnit, Algebra.basicOpen_subset_smoothLocus_iff_smooth, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, mem_image_comap_basicOpen, basicOpen_zero, isClopen_iff, AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen, Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, Algebra.basicOpen_subset_etaleLocus_iff, isOpen_basicOpen, exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen, isTopologicalBasis_basic_opens, basicOpen_mul_le_left, exists_idempotent_basicOpen_eq_of_isClopen, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine_isIso, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, isClopen_basicOpen_of_mul_add, isIdempotentElemEquivClopens_apply_toOpens, basicOpen_isIdempotentElemEquivClopens_symm, Polynomial.image_comap_C_basicOpen, comap_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map, AlgebraicGeometry.basicOpen_eq_of_affine', AlgebraicGeometry.Proj.awayι_preimage_basicOpen, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc, AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, basicOpen_eq_zeroLocus_compl, AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen, isCompact_basicOpen, basicOpen_mul_le_right, existsUnique_idempotent_basicOpen_eq_of_isClopen, basicOpen_le_basicOpen_iff, mem_basicOpen, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen, AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.Scheme.affineBasisCover_map_range, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, zeroLocus_eq_basicOpen_of_mul_add, AlgebraicGeometry.StructureSheaf.instAwayObjOppositeOpensCarrierTopValStructureSheafInTypeOpBasicOpen, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_app_spec_assoc, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_spec, basicOpen_one, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen, iSup_basicOpen_eq_top_iff', Algebra.basicOpen_subset_smoothLocus_iff, AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, localization_away_comap_range, isRetrocompact_basicOpen, coe_isIdempotentElemEquivClopens_apply, isBasis_basic_opens, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, MvPolynomial.mem_image_comap_C_basicOpen, basicOpen_eq_bot_iff, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecModuleCatPresheafModulesSheafModulesSpecToSheafOpBasicOpenPowersHomToOpen, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCApp_iff, AlgebraicGeometry.IsAffineOpen.Spec_basicOpen
closedsEmbedding 📖	CompOp	—
homeomorphOfRingEquiv 📖	CompOp	—
isIdempotentElemEquivClopens 📖	CompOp	10 math math: isIdempotentElemEquivClopens_symm_bot, isIdempotentElemEquivClopens_one_sub, isIdempotentElemEquivClopens_symm_inf, isIdempotentElemEquivClopens_symm_sup, isIdempotentElemEquivClopens_apply_toOpens, basicOpen_isIdempotentElemEquivClopens_symm, isIdempotentElemEquivClopens_symm_top, isIdempotentElemEquivClopens_mul, coe_isIdempotentElemEquivClopens_apply, isIdempotentElemEquivClopens_symm_compl
localizationMapOfSpecializes 📖	CompOp	—
mulZeroAddOneEquivClopens 📖	CompOp	—
nhdsOrderEmbedding 📖	CompOp	1 math math: nhdsOrderEmbedding_apply
pointsEquivIrreducibleCloseds 📖	CompOp	—
primeSpectrumProdHomeo 📖	CompOp	—
zariskiTopology 📖	CompOp	177 math math: closure_range_comap, isClopen_iff_mul_add, vanishingIdeal_isClosed_isIrreducible, Polynomial.mem_image_comap_C_basicOpen, isOpenMap_comap_of_hasGoingDown_of_finitePresentation, LocalizedModule.subsingleton_iff_disjoint, discreteTopology_iff_finite_and_krullDimLE_zero, AlgebraicGeometry.Polynomial.isOpenMap_comap_C, isClosedEmbedding_comap_snd, MvPolynomial.isOpenMap_comap_C, isClosed_zeroLocus, isClopen_iff_mul_add_zeroLocus, localization_comap_isInducing, isHomeomorph_comap, isRetrocompact_zeroLocus_compl_of_fg, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_apply, discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, basicOpen_injOn_isIdempotentElem, denseRange_comap_iff_ker_le_nilRadical, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal, MvPolynomial.image_comap_C_basicOpen, instDiscreteTopology, isClosed_iff_zeroLocus, Algebra.basicOpen_subset_etaleLocus_iff_etale, IsLocalRing.closedPoint_mem_iff, basicOpen_eq_zeroLocus_of_mul_add, Module.basicOpen_subset_freeLocus_iff, instQuasiSoberElemZeroLocus, localization_away_isOpenEmbedding, AlgebraicGeometry.StructureSheaf.exists_const, denseRange_comap_iff_minimalPrimes, Algebra.basicOpen_subset_unramifiedLocus_iff, RingHom.Flat.generalizingMap_comap, instT0Space, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, Algebra.QuasiFiniteAt.isClopen_singleton, vanishingIdeal_irreducibleComponents, isCompact_isOpen_iff, IsLocalRing.isClosed_singleton_closedPoint, instQuasiSeparatedSpace, coe_preimageHomeomorphFiber_apply_asIdeal, le_basicOpen_pow, iSup_basicOpen_eq_top_iff, Algebra.QuasiFinite.isDiscrete_comap_preimage_singleton, isEmbedding_tensorProductTo_of_surjectiveOnStalks, isConstructible_basicOpen, basicOpen_mul, isClosed_iff_zeroLocus_radical_ideal, basicOpen_eq_zeroLocus_of_isIdempotentElem, quasiSober, instSpectralSpace, t1Space_iff_isField, zeroLocus_eq_basicOpen_of_isIdempotentElem, isIdempotentElemEquivClopens_symm_bot, isIrreducible_zeroLocus_iff_of_radical, discreteTopology_of_toLocalization_surjective, isOpenMap_comap_algebraMap_tensorProduct_of_field, isIdempotentElemEquivClopens_one_sub, basicOpen_le_basicOpen_iff_algebraMap_isUnit, zeroLocus_minimalPrimes, isIrreducible_zeroLocus_iff, AlgebraicGeometry.IsPreimmersion.Spec_map_iff, Algebra.basicOpen_subset_smoothLocus_iff_smooth, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_continuous, mem_image_comap_basicOpen, isClosedEmbedding_comap_fst, basicOpen_zero, isClopen_iff, Polynomial.isOpen_image_comap_of_monic, isClosedMap_comap_of_isIntegral, isIdempotentElemEquivClopens_symm_inf, MaximalSpectrum.toPrimeSpectrum_continuous, continuous_comap, AlgebraicGeometry.StructureSheaf.toOpen_comp_comap_assoc, Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, Algebra.isOpen_etaleLocus, ConstructibleSetData.isConstructible_toSet, vanishingIdeal_isIrreducible, Polynomial.isOpenMap_comap_C, zeroLocus_ideal_mem_irreducibleComponents, Algebra.quasiFiniteAt_iff_isOpen_singleton_fiber, isClosed_singleton_iff_isMaximal, isOpen_iff, IsLocalRing.specializes_closedPoint, Algebra.isOpen_smoothLocus, Module.isOpen_freeLocus, Algebra.basicOpen_subset_etaleLocus_iff, exists_constructibleSetData_iff, le_iff_mem_closure, compactSpace, isIdempotentElemEquivClopens_symm_sup, discreteTopology_iff_toPiLocalization_surjective, isClosed_iff_zeroLocus_ideal, Polynomial.isCompact_image_comap_of_monic, isOpen_basicOpen, instPrespectralSpace, Module.isLocallyConstant_rankAtStalk_freeLocus, isTopologicalBasis_basic_opens, basicOpen_mul_le_left, nhdsOrderEmbedding_apply, isHomeomorph_comap_of_isPurelyInseparable, stableUnderSpecialization_range_iff, closure_image_comap_zeroLocus, IsLocalRing.closed_point_mem_iff, le_iff_specializes, instNoetherianSpace, closure_singleton, isClopen_basicOpen_of_mul_add, isIdempotentElemEquivClopens_apply_toOpens, basicOpen_isIdempotentElemEquivClopens_symm, stableUnderSpecialization_singleton, Polynomial.image_comap_C_basicOpen, isRetrocompact_zeroLocus_compl, comap_basicOpen, Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap, AlgebraicGeometry.IsPreimmersion.SpecMap_iff, Algebra.isOpen_unramifiedLocus, MaximalSpectrum.toPrimeSpectrum_range, AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal, topologicalKrullDim_eq_ringKrullDim, Module.isLocallyConstant_rankAtStalk, isIdempotentElemEquivClopens_symm_top, stableUnderGeneralization_singleton, comap_singleton_isClosed_of_surjective, irreducibleSpace, basicOpen_eq_zeroLocus_compl, isCompact_basicOpen, basicOpen_mul_le_right, isHomeomorph_comap_tensorProductMap_of_isPurelyInseparable, basicOpen_le_basicOpen_iff, Algebra.QuasiFinite.discreteTopology_primeSpectrum, mem_basicOpen, continuous_tensorProductTo, AlgebraicGeometry.Spec.map_base, isClopen_iff_zeroLocus, isEmbedding_comap_of_surjective, coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, Module.stableUnderSpecialization_support, isIrreducible_iff_vanishingIdeal_isPrime, AlgebraicGeometry.StructureSheaf.comap_basicOpen, AlgebraicGeometry.Scheme.affineBasisCover_map_range, isClosed_range_comap_of_surjective, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_preimage_basicOpen, zeroLocus_eq_basicOpen_of_mul_add, AlgebraicGeometry.Polynomial.isOpen_imageOfDf, isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing, instJacobsonSpaceOfIsJacobsonRing, isJacobsonRing_iff_jacobsonSpace, AlgebraicGeometry.LocallyRingedSpace.toΓSpecCBasicOpens_app, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen, Module.isClosed_support, localization_comap_isEmbedding, basicOpen_one, iSup_basicOpen_eq_top_iff', isClosed_comap_singleton_of_isIntegral, Algebra.basicOpen_subset_smoothLocus_iff, vanishingIdeal_closure, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen, isClosedEmbedding_comap_of_surjective, isIdempotentElemEquivClopens_mul, localization_away_comap_range, isRetrocompact_basicOpen, coe_isIdempotentElemEquivClopens_apply, isCompact_isOpen_iff_ideal, isIdempotentElemEquivClopens_symm_compl, isBasis_basic_opens, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq, vanishingIdeal_mem_minimalPrimes, zeroLocus_vanishingIdeal_eq_closure, comap_isInducing_of_surjective, discreteTopology_iff_toPiLocalization_bijective, isHomeomorph_comap_of_bijective, MvPolynomial.mem_image_comap_C_basicOpen, stableUnderSpecialization_image_iff, basicOpen_eq_bot_iff, isConstructible_range_comap
zeroLocusEquivIrreducibleCloseds 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
basicOpen_eq_bot_iff 📖	mathematical	—	basicOpen Bot.bot TopologicalSpace.Opens PrimeSpectrum zariskiTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot IsNilpotent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	basicOpen_eq_zeroLocus_compl
basicOpen_eq_zeroLocus_compl 📖	mathematical	—	SetLike.coe TopologicalSpace.Opens PrimeSpectrum zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen Compl.compl Set Set.instCompl zeroLocus Set.instSingletonSet	—	Set.ext
basicOpen_eq_zeroLocus_of_isIdempotentElem 📖	mathematical	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	SetLike.coe TopologicalSpace.Opens PrimeSpectrum CommRing.toCommSemiring zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen zeroLocus Set Set.instSingletonSet SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	basicOpen_eq_zeroLocus_of_mul_add mul_sub mul_one IsIdempotentElem.eq sub_self add_sub_cancel
basicOpen_eq_zeroLocus_of_mul_add 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	SetLike.coe TopologicalSpace.Opens PrimeSpectrum zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen zeroLocus Set Set.instSingletonSet	—	Set.ext Ideal.IsPrime.mem_or_mem_of_mul_eq_zero isPrime Ideal.IsPrime.ne_top' Ideal.eq_top_iff_one AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass basicOpen_eq_zeroLocus_compl
basicOpen_injOn_isIdempotentElem 📖	mathematical	—	Set.InjOn TopologicalSpace.Opens PrimeSpectrum zariskiTopology basicOpen setOf IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Ideal.mem_span_singleton' mul_assoc Ideal.exists_le_prime_notMem_of_isIdempotentElem Ideal.span_singleton_le_iff_mem mul_comm of_not_not
basicOpen_isIdempotentElemEquivClopens_symm 📖	mathematical	—	basicOpen CommRing.toCommSemiring IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe OrderIso TopologicalSpace.Clopens PrimeSpectrum zariskiTopology Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Clopens.instPartialOrder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring instFunLikeOrderIso OrderIso.symm isIdempotentElemEquivClopens TopologicalSpace.Clopens.toOpens	—	TopologicalSpace.Opens.ext OrderIso.apply_symm_apply
basicOpen_le_basicOpen_iff 📖	mathematical	—	TopologicalSpace.Opens PrimeSpectrum zariskiTopology Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder basicOpen Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.radical Ideal.span Set Set.instSingletonSet	—	SetLike.coe_subset_coe instIsConcreteLE basicOpen_eq_zeroLocus_compl Set.compl_subset_compl zeroLocus_subset_zeroLocus_singleton_iff
basicOpen_le_basicOpen_iff_algebraMap_isUnit 📖	mathematical	—	TopologicalSpace.Opens PrimeSpectrum zariskiTopology Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder basicOpen IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	IsLocalization.Away.algebraMap_isUnit_iff
basicOpen_mul 📖	mathematical	—	basicOpen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring TopologicalSpace.Opens PrimeSpectrum zariskiTopology SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice	—	TopologicalSpace.Opens.ext basicOpen_eq_zeroLocus_compl zeroLocus_singleton_mul Set.compl_union
basicOpen_mul_le_left 📖	mathematical	—	TopologicalSpace.Opens PrimeSpectrum zariskiTopology Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder basicOpen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	basicOpen_mul inf_le_left
basicOpen_mul_le_right 📖	mathematical	—	TopologicalSpace.Opens PrimeSpectrum zariskiTopology Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder basicOpen Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	basicOpen_mul inf_le_right
basicOpen_one 📖	mathematical	—	basicOpen AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring Top.top TopologicalSpace.Opens PrimeSpectrum zariskiTopology OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	TopologicalSpace.Opens.ext basicOpen_eq_zeroLocus_compl zeroLocus_singleton_one Set.compl_empty
basicOpen_pow 📖	mathematical	—	basicOpen Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	TopologicalSpace.Opens.ext basicOpen_eq_zeroLocus_compl zeroLocus_singleton_pow
basicOpen_zero 📖	mathematical	—	basicOpen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Bot.bot TopologicalSpace.Opens PrimeSpectrum zariskiTopology OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra TopologicalSpace.Opens.instFrame HeytingAlgebra.toOrderBot	—	TopologicalSpace.Opens.ext basicOpen_eq_zeroLocus_compl zeroLocus_singleton_zero Set.compl_univ
closure_image_comap_zeroLocus 📖	mathematical	—	closure PrimeSpectrum CommRing.toCommSemiring zariskiTopology Set.image comap zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.comap RingHom RingHom.instFunLike RingHom.instRingHomClass	—	subset_antisymm RingHom.instRingHomClass Set.instAntisymmSubset IsClosed.closure_subset_iff isClosed_zeroLocus Set.image_subset_iff preimage_comap_zeroLocus zeroLocus_anti_mono Set.image_preimage_subset Ideal.exists_minimalPrimes_le isPrime Ideal.exists_comap_eq_of_mem_minimalPrimes IsClosed.stableUnderSpecialization isClosed_closure le_iff_specializes subset_closure
closure_range_comap 📖	mathematical	—	closure PrimeSpectrum zariskiTopology Set.range comap zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass	—	RingHom.instRingHomClass zeroLocus_vanishingIdeal_eq_closure vanishingIdeal_range_comap zeroLocus_radical
closure_singleton 📖	mathematical	—	closure PrimeSpectrum zariskiTopology Set Set.instSingletonSet zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	zeroLocus_vanishingIdeal_eq_closure vanishingIdeal_singleton
coe_isIdempotentElemEquivClopens_apply 📖	mathematical	—	SetLike.coe TopologicalSpace.Clopens PrimeSpectrum CommRing.toCommSemiring zariskiTopology TopologicalSpace.Clopens.instSetLike DFunLike.coe OrderIso IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring TopologicalSpace.Clopens.instPartialOrder instFunLikeOrderIso isIdempotentElemEquivClopens TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	—
comap_apply 📖	mathematical	—	comap	—	—
comap_basicOpen 📖	mathematical	—	DFunLike.coe FrameHom TopologicalSpace.Opens PrimeSpectrum zariskiTopology TopologicalSpace.Opens.instCompleteLattice FrameHom.instFunLike TopologicalSpace.Opens.comap comap continuous_comap basicOpen RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	—	continuous_comap
comap_isInducing_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	Topology.IsInducing PrimeSpectrum zariskiTopology comap	—	preimage_comap_zeroLocus Function.Surjective.image_preimage
comap_quotientMk_bijective_of_le_nilradical 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule nilradical	Function.Bijective PrimeSpectrum HasQuotient.Quotient Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.commSemiring comap Ideal.instIsTwoSided_1	—	Ideal.instIsTwoSided_1 comap_injective_of_surjective Ideal.Quotient.mk_surjective RingHom.instRingHomClass range_comap_of_surjective Ideal.mk_ker instIsConcreteLE
comap_singleton_isClosed_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	IsClosed PrimeSpectrum zariskiTopology Set Set.instSingletonSet comap	—	isClosed_singleton_iff_isMaximal Ideal.comap_isMaximal_of_surjective RingHom.instRingHomClass
compactSpace 📖	mathematical	—	CompactSpace PrimeSpectrum zariskiTopology	—	compactSpace_of_finite_subfamily_closed Set.iInter_congr_Prop CompleteLattice.IsCompactElement.exists_finset_of_le_iSup Ideal.isCompactElement_top isClosed_iff_zeroLocus_ideal
continuous_comap 📖	mathematical	—	Continuous PrimeSpectrum zariskiTopology comap	—	preimage_comap_zeroLocus_aux
denseRange_comap_iff_ker_le_nilRadical 📖	mathematical	—	DenseRange PrimeSpectrum zariskiTopology comap Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass nilradical	—	RingHom.instRingHomClass denseRange_iff_closure_range closure_range_comap zeroLocus_eq_univ_iff SetLike.coe_subset_coe instIsConcreteLE
denseRange_comap_iff_minimalPrimes 📖	mathematical	—	DenseRange PrimeSpectrum zariskiTopology comap Set Set.instMembership Set.range Ideal.IsPrime CommSemiring.toSemiring Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Bot.bot Submodule.instBot	—	RingHom.instRingHomClass bot_le LE.le.trans denseRange_comap_iff_ker_le_nilRadical Ideal.IsPrime.radical_le_iff Ideal.exists_comap_eq_of_mem_minimalPrimes Ideal.exists_minimalPrimes_le isPrime Specializes.mem_closed le_iff_specializes isClosed_closure subset_closure
discreteTopology_iff_finite_and_krullDimLE_zero 📖	mathematical	—	DiscreteTopology PrimeSpectrum zariskiTopology Finite Ring.KrullDimLE	—	finite_of_compact_of_discrete compactSpace Ring.KrullDimLE.mk₀ isClosed_singleton_iff_isMaximal discreteTopology_iff_forall_isClosed DiscreteTopology.of_finite_of_isClosed_singleton instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat isPrime
discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical 📖	mathematical	—	DiscreteTopology PrimeSpectrum zariskiTopology Finite Set.Elem Ideal CommSemiring.toSemiring setOf Ideal.IsMaximal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule InfSet.sInf Submodule.instInfSet nilradical	—	discreteTopology_iff_finite_and_krullDimLE_zero Ring.krullDimLE_zero_iff Equiv.finite_iff Set.coe_setOf Set.finite_coe_iff Set.Finite.subset Ideal.IsMaximal.isPrime sInf_le_sInf nilradical_eq_sInf LE.le.trans nilradical_le_prime Ideal.IsPrime.inf_le' Finset.inf_id_eq_sInf Set.Finite.coe_toFinset Ideal.IsMaximal.eq_of_le Set.Finite.mem_toFinset Ideal.IsPrime.ne_top'
discreteTopology_iff_toPiLocalization_bijective 📖	mathematical	—	DiscreteTopology PrimeSpectrum zariskiTopology Function.Bijective PiLocalization DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.nonAssocSemiring Localization CommSemiring.toCommMonoid Ideal.primeCompl asIdeal isPrime OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.instFunLike toPiLocalization	—	isPrime discreteTopology_iff_toPiLocalization_surjective toPiLocalization_injective
discreteTopology_iff_toPiLocalization_surjective 📖	mathematical	—	DiscreteTopology PrimeSpectrum zariskiTopology PiLocalization DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.nonAssocSemiring Localization CommSemiring.toCommMonoid Ideal.primeCompl asIdeal isPrime OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.instFunLike toPiLocalization	—	isPrime toPiLocalization_surjective_of_discreteTopology discreteTopology_of_toLocalization_surjective
discreteTopology_of_toLocalization_surjective 📖	mathematical	PiLocalization DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.nonAssocSemiring PrimeSpectrum Localization CommSemiring.toCommMonoid Ideal.primeCompl asIdeal isPrime OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.instFunLike toPiLocalization	DiscreteTopology zariskiTopology	—	isPrime discreteTopology_iff_finite_and_krullDimLE_zero finite_of_toPiLocalization_surjective Ring.KrullDimLE.mk₀ isMaximal_of_toPiLocalization_surjective
eq_biUnion_of_isOpen 📖	mathematical	IsOpen PrimeSpectrum zariskiTopology	Set.iUnion Set Set.instHasSubset SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' isTopologicalBasis_basic_opens basicOpen_eq_zeroLocus_compl Set.iUnion_congr_Prop Set.ext
existsUnique_idempotent_basicOpen_eq_of_isClopen 📖	mathematical	IsClopen PrimeSpectrum zariskiTopology	ExistsUnique IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Set SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	existsUnique_of_exists_of_unique exists_idempotent_basicOpen_eq_of_isClopen basicOpen_injOn_isIdempotentElem SetLike.ext'
exists_idempotent_basicOpen_eq_of_isClopen 📖	mathematical	IsClopen PrimeSpectrum zariskiTopology	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen IsIdempotentElem.of_mul_add
exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen 📖	mathematical	IsClopen PrimeSpectrum zariskiTopology	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen Compl.compl Set Set.instCompl	—	subsingleton_or_nontrivial Unique.instSubsingleton instIsEmptyOfSubsingleton isCompact_isOpen_iff_ideal IsClosed.isCompact compactSpace IsOpen.isClosed_compl IsClosed.isOpen_compl IsScalarTower.right Ideal.radical_le_radical_iff le_of_eq zeroLocus_eq_iff Ideal.zero_eq_bot zeroLocus_bot zeroLocus_mul compl_compl Set.compl_union_self Ideal.exists_pow_le_of_le_radical_of_fg Submodule.FG.mul pow_zero Ideal.one_eq_top Ideal.instNontrivial eq_top_iff Ideal.span_pow_eq_top Ideal.span_union Ideal.span_eq zeroLocus_empty_iff_eq_top zeroLocus_sup Set.compl_inter_self Ideal.span_le Set.image_union Set.union_subset_iff Ideal.mem_sup_left Ideal.pow_mem_pow Ideal.mem_sup_right Submodule.mem_sup Ideal.eq_top_iff_one mul_pow Ideal.mul_mem_mul subset_antisymm Set.instAntisymmSubset basicOpen_eq_zeroLocus_of_mul_add zeroLocus_anti_mono Set.singleton_subset_iff Ideal.pow_le_self basicOpen_eq_zeroLocus_compl Set.compl_subset_comm
iSup_basicOpen_eq_top_iff 📖	mathematical	—	iSup TopologicalSpace.Opens PrimeSpectrum zariskiTopology ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice basicOpen Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Ideal.span CommSemiring.toSemiring Set.range Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	SetLike.ext'_iff TopologicalSpace.Opens.coe_iSup basicOpen_eq_zeroLocus_compl zeroLocus_empty_iff_eq_top Function.Involutive.eq_iff compl_involutive Set.iUnion_singleton_eq_range Set.compl_univ zeroLocus_span
iSup_basicOpen_eq_top_iff' 📖	mathematical	—	iSup TopologicalSpace.Opens PrimeSpectrum zariskiTopology ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.Opens.instCompleteLattice Set Set.instMembership basicOpen Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Ideal.span CommSemiring.toSemiring Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Subtype.range_val iSup_basicOpen_eq_top_iff isOpen_iUnion TopologicalSpace.Opens.is_open' Set.iUnion_congr_Prop basicOpen_eq_zeroLocus_compl Set.iUnion_coe_set
instPrespectralSpace 📖	mathematical	—	PrespectralSpace PrimeSpectrum zariskiTopology	—	PrespectralSpace.of_isTopologicalBasis' isTopologicalBasis_basic_opens isCompact_basicOpen
instQuasiSeparatedSpace 📖	mathematical	—	QuasiSeparatedSpace PrimeSpectrum zariskiTopology	—	QuasiSeparatedSpace.of_isTopologicalBasis isTopologicalBasis_basic_opens isCompact_basicOpen
instQuasiSoberElemZeroLocus 📖	mathematical	—	QuasiSober Set.Elem PrimeSpectrum zeroLocus instTopologicalSpaceSubtype Set Set.instMembership zariskiTopology	—	Topology.IsClosedEmbedding.quasiSober IsClosed.isClosedEmbedding_subtypeVal isClosed_zeroLocus quasiSober
instSpectralSpace 📖	mathematical	—	SpectralSpace PrimeSpectrum zariskiTopology	—	instT0Space compactSpace quasiSober instQuasiSeparatedSpace instPrespectralSpace
instT0Space 📖	mathematical	—	T0Space PrimeSpectrum zariskiTopology	—	Function.Embedding.inj'
irreducibleSpace 📖	mathematical	—	IrreducibleSpace PrimeSpectrum zariskiTopology	—	irreducibleSpace_def Set.top_eq_univ zeroLocus_bot isIrreducible_zeroLocus_iff Ideal.radical_bot_of_noZeroDivisors IsDomain.to_noZeroDivisors Ideal.isPrime_bot IsDomain.toNontrivial
isBasis_basic_opens 📖	mathematical	—	TopologicalSpace.Opens.IsBasis PrimeSpectrum zariskiTopology Set.range TopologicalSpace.Opens basicOpen	—	Set.range_comp isTopologicalBasis_basic_opens
isClopen_basicOpen_of_mul_add 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	IsClopen PrimeSpectrum zariskiTopology SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	isClosed_zeroLocus basicOpen_eq_zeroLocus_of_mul_add TopologicalSpace.Opens.is_open'
isClopen_iff 📖	mathematical	—	IsClopen PrimeSpectrum CommRing.toCommSemiring zariskiTopology IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	exists_idempotent_basicOpen_eq_of_isClopen basicOpen_eq_zeroLocus_of_isIdempotentElem isClosed_zeroLocus TopologicalSpace.Opens.is_open'
isClopen_iff_mul_add 📖	mathematical	—	IsClopen PrimeSpectrum zariskiTopology Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen isClopen_basicOpen_of_mul_add
isClopen_iff_mul_add_zeroLocus 📖	mathematical	—	IsClopen PrimeSpectrum zariskiTopology Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne zeroLocus Set Set.instSingletonSet	—	isClopen_iff_mul_add exists_swap mul_comm add_comm zeroLocus_eq_basicOpen_of_mul_add
isClopen_iff_zeroLocus 📖	mathematical	—	IsClopen PrimeSpectrum CommRing.toCommSemiring zariskiTopology IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing zeroLocus Set Set.instSingletonSet	—	isClopen_iff IsIdempotentElem.one_sub basicOpen_eq_zeroLocus_of_isIdempotentElem zeroLocus_eq_basicOpen_of_isIdempotentElem
isClosedEmbedding_comap_fst 📖	mathematical	—	Topology.IsClosedEmbedding PrimeSpectrum Prod.instCommSemiring zariskiTopology comap RingHom.fst Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Topology.isClosedEmbedding_iff isEmbedding_comap_of_surjective Prod.fst_surjective Zero.instNonempty RingHom.instRingHomClass range_comap_fst
isClosedEmbedding_comap_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	Topology.IsClosedEmbedding PrimeSpectrum zariskiTopology comap	—	comap_isInducing_of_surjective comap_injective_of_surjective isClosed_range_comap_of_surjective
isClosedEmbedding_comap_snd 📖	mathematical	—	Topology.IsClosedEmbedding PrimeSpectrum Prod.instCommSemiring zariskiTopology comap RingHom.snd Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Topology.isClosedEmbedding_iff isEmbedding_comap_of_surjective Prod.snd_surjective Zero.instNonempty RingHom.instRingHomClass range_comap_snd
isClosedMap_comap_of_isIntegral 📖	mathematical	RingHom.IsIntegral CommRing.toRing	IsClosedMap PrimeSpectrum CommRing.toCommSemiring zariskiTopology comap	—	isClosed_image_of_stableUnderSpecialization RingHom.instRingHomClass Ideal.exists_ideal_over_prime_of_isIntegral isPrime le_iff_specializes Specializes.mem_closed ext
isClosed_comap_singleton_of_isIntegral 📖	mathematical	RingHom.IsIntegral CommRing.toRing	IsClosed PrimeSpectrum CommRing.toCommSemiring zariskiTopology Set Set.instSingletonSet comap	—	Set.image_singleton isClosedMap_comap_of_isIntegral
isClosed_iff_zeroLocus 📖	mathematical	—	IsClosed PrimeSpectrum zariskiTopology zeroLocus	—	isOpen_compl_iff isOpen_iff compl_compl
isClosed_iff_zeroLocus_ideal 📖	mathematical	—	IsClosed PrimeSpectrum zariskiTopology zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	isClosed_iff_zeroLocus zeroLocus_span
isClosed_iff_zeroLocus_radical_ideal 📖	mathematical	—	IsClosed PrimeSpectrum zariskiTopology Ideal.IsRadical zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	isClosed_iff_zeroLocus_ideal Ideal.radical_isRadical zeroLocus_radical
isClosed_image_of_stableUnderSpecialization 📖	mathematical	StableUnderSpecialization PrimeSpectrum zariskiTopology Set.image comap	IsClosed	—	isClosed_iff_zeroLocus_ideal isClosed_iff_zeroLocus RingHom.instRingHomClass le_antisymm Ideal.comap_mono Ideal.exists_ideal_comap_le_prime isPrime Ideal.IsPrime.comap le_iff_specializes
isClosed_range_comap_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	IsClosed PrimeSpectrum zariskiTopology Set.range comap	—	RingHom.instRingHomClass range_comap_of_surjective isClosed_zeroLocus
isClosed_range_of_stableUnderSpecialization 📖	mathematical	StableUnderSpecialization PrimeSpectrum zariskiTopology Set.range comap	IsClosed	—	Set.image_univ isClosed_image_of_stableUnderSpecialization isClosed_univ
isClosed_singleton_iff_isMaximal 📖	mathematical	—	IsClosed PrimeSpectrum zariskiTopology Set Set.instSingletonSet Ideal.IsMaximal CommSemiring.toSemiring asIdeal	—	closure_subset_iff_isClosed zeroLocus_vanishingIdeal_eq_closure vanishingIdeal_singleton Ideal.exists_le_maximal Ideal.IsPrime.ne_top' isPrime Ideal.IsMaximal.isPrime ext Ideal.IsMaximal.eq_of_le
isClosed_zeroLocus 📖	mathematical	—	IsClosed PrimeSpectrum zariskiTopology zeroLocus	—	isClosed_iff_zeroLocus
isCompact_basicOpen 📖	mathematical	—	IsCompact PrimeSpectrum zariskiTopology SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	localization_away_comap_range Localization.isLocalization isCompact_range compactSpace continuous_comap
isCompact_isOpen_iff 📖	mathematical	—	IsCompact PrimeSpectrum zariskiTopology IsOpen Compl.compl Set Set.instCompl zeroLocus SetLike.coe Finset Finset.instSetLike	—	isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis isTopologicalBasis_basic_opens isCompact_basicOpen Set.iUnion_congr_Prop basicOpen_eq_zeroLocus_compl Set.biUnion_of_singleton Set.Finite.coe_toFinset Finset.finite_toSet
isCompact_isOpen_iff_ideal 📖	mathematical	—	IsCompact PrimeSpectrum zariskiTopology IsOpen Ideal.FG CommSemiring.toSemiring Compl.compl Set Set.instCompl zeroLocus SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	isCompact_isOpen_iff zeroLocus_span
isConstructible_basicOpen 📖	mathematical	—	Topology.IsConstructible PrimeSpectrum zariskiTopology SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	IsRetrocompact.isConstructible TopologicalSpace.Opens.is_open' isRetrocompact_basicOpen
isEmbedding_comap_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	Topology.IsEmbedding PrimeSpectrum zariskiTopology comap	—	Topology.isEmbedding_iff comap_isInducing_of_surjective comap_injective_of_surjective
isHomeomorph_comap_of_bijective 📖	mathematical	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike	IsHomeomorph PrimeSpectrum zariskiTopology comap	—	Homeomorph.isHomeomorph RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
isIdempotentElemEquivClopens_apply_toOpens 📖	mathematical	—	TopologicalSpace.Clopens.toOpens PrimeSpectrum CommRing.toCommSemiring zariskiTopology DFunLike.coe OrderIso IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TopologicalSpace.Clopens Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring TopologicalSpace.Clopens.instPartialOrder instFunLikeOrderIso isIdempotentElemEquivClopens basicOpen	—	—
isIdempotentElemEquivClopens_mul 📖	mathematical	—	DFunLike.coe OrderIso IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TopologicalSpace.Clopens PrimeSpectrum CommRing.toCommSemiring zariskiTopology Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring TopologicalSpace.Clopens.instPartialOrder instFunLikeOrderIso isIdempotentElemEquivClopens CommMagma.toMul CommSemigroup.toCommMagma Set Set.instMembership setOf IsIdempotentElem.mul TopologicalSpace.Clopens.instMin	—	InfHomClass.map_inf InfTopHomClass.toInfHomClass OrderIsoClass.toInfTopHomClass OrderIso.instOrderIsoClass
isIdempotentElemEquivClopens_one_sub 📖	mathematical	—	DFunLike.coe OrderIso IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing TopologicalSpace.Clopens PrimeSpectrum CommRing.toCommSemiring zariskiTopology Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring TopologicalSpace.Clopens.instPartialOrder instFunLikeOrderIso isIdempotentElemEquivClopens SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Set Set.instMembership setOf IsIdempotentElem.one_sub Compl.compl TopologicalSpace.Clopens.instCompl	—	map_compl OrderIsoClass.toHeytingHomClass OrderIso.instOrderIsoClass
isIdempotentElemEquivClopens_symm_bot 📖	mathematical	—	DFunLike.coe OrderIso TopologicalSpace.Clopens PrimeSpectrum CommRing.toCommSemiring zariskiTopology IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Clopens.instPartialOrder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring instFunLikeOrderIso OrderIso.symm isIdempotentElemEquivClopens Bot.bot TopologicalSpace.Clopens.instBot MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass IsIdempotentElem.zero	—	BotHomClass.map_bot SupBotHomClass.toBotHomClass OrderIsoClass.toSupBotHomClass OrderIso.instOrderIsoClass
isIdempotentElemEquivClopens_symm_compl 📖	mathematical	—	DFunLike.coe OrderIso TopologicalSpace.Clopens PrimeSpectrum CommRing.toCommSemiring zariskiTopology IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Clopens.instPartialOrder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring instFunLikeOrderIso OrderIso.symm isIdempotentElemEquivClopens Compl.compl TopologicalSpace.Clopens.instCompl SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne IsIdempotentElem.one_sub	—	map_compl OrderIsoClass.toHeytingHomClass OrderIso.instOrderIsoClass
isIdempotentElemEquivClopens_symm_inf 📖	mathematical	—	DFunLike.coe OrderIso TopologicalSpace.Clopens PrimeSpectrum CommRing.toCommSemiring zariskiTopology IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Clopens.instPartialOrder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring instFunLikeOrderIso OrderIso.symm isIdempotentElemEquivClopens TopologicalSpace.Clopens.instMin CommMagma.toMul CommSemigroup.toCommMagma IsIdempotentElem.mul	—	InfHomClass.map_inf InfTopHomClass.toInfHomClass OrderIsoClass.toInfTopHomClass OrderIso.instOrderIsoClass
isIdempotentElemEquivClopens_symm_sup 📖	mathematical	—	DFunLike.coe OrderIso TopologicalSpace.Clopens PrimeSpectrum CommRing.toCommSemiring zariskiTopology IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Clopens.instPartialOrder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring instFunLikeOrderIso OrderIso.symm isIdempotentElemEquivClopens TopologicalSpace.Clopens.instMax SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd IsIdempotentElem.add_sub_mul	—	SupHomClass.map_sup SupBotHomClass.toSupHomClass OrderIsoClass.toSupBotHomClass OrderIso.instOrderIsoClass
isIdempotentElemEquivClopens_symm_top 📖	mathematical	—	DFunLike.coe OrderIso TopologicalSpace.Clopens PrimeSpectrum CommRing.toCommSemiring zariskiTopology IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Clopens.instPartialOrder SemilatticeInf.toPartialOrder instSemilatticeInfSubtypeIsIdempotentElem NonUnitalCommSemiring.toCommSemigroup NonUnitalCommRing.toNonUnitalCommSemiring instFunLikeOrderIso OrderIso.symm isIdempotentElemEquivClopens Top.top TopologicalSpace.Clopens.instTop AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing IsIdempotentElem.one MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	TopHomClass.map_top InfTopHomClass.toTopHomClass OrderIsoClass.toInfTopHomClass OrderIso.instOrderIsoClass
isIntegral_of_isClosedMap_comap_mapRingHom 📖	mathematical	IsClosedMap PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring zariskiTopology comap Polynomial.mapRingHom	RingHom.IsIntegral CommRing.toRing	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Algebra.IsIntegral.of_finite Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite isNoetherian_of_subsingleton isNoetherian_of_finite Finite.of_subsingleton RingHom.instRingHomClass isClosed_zeroLocus Ideal.eq_top_iff_one sup_comm zeroLocus_empty_iff_eq_top zeroLocus_sup closure_image_comap_zeroLocus closure_eq_iff_isClosed zeroLocus_span sub_sub_cancel sub_mem Submodule.addSubgroupClass Ideal.mul_mem_left Ideal.IsPrime.ne_top isPrime Polynomial.map_X Ideal.mem_span_singleton_sup Ideal.mem_span_singleton Polynomial.Monic.mul Polynomial.coeff_add Polynomial.mul_coeff_zero Polynomial.coeff_X_zero MulZeroClass.mul_zero zero_add Polynomial.coeff_one_zero NeZero.one Polynomial.Monic.def Polynomial.reverse_leadingCoeff Polynomial.trailingCoeff.eq_1 map_neg RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Polynomial.natDegree_linear_le Polynomial.eval₂_eq_eval_map Polynomial.reverse.eq_1 Polynomial.map_mul Polynomial.reflect_map Polynomial.map_pow Polynomial.revAt_zero Polynomial.reflect_monomial Polynomial.reflect_mul Polynomial.natDegree_map_le pow_zero Polynomial.natDegree_one Nat.instCanonicallyOrderedAdd mul_one add_assoc LE.le.trans covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le le_rfl Polynomial.eval_mul Polynomial.reflect_sub Polynomial.natDegree_C Polynomial.natDegree_X Polynomial.reflect_C Polynomial.reflect_one_X Polynomial.reflect_one Polynomial.eval_sub Polynomial.eval_C Polynomial.eval_pow Polynomial.eval_X sub_self MulZeroClass.zero_mul Algebra.isIntegral_def
isIrreducible_iff_vanishingIdeal_isPrime 📖	mathematical	—	IsIrreducible PrimeSpectrum zariskiTopology Ideal.IsPrime CommSemiring.toSemiring vanishingIdeal	—	isIrreducible_iff_closure zeroLocus_vanishingIdeal_eq_closure isIrreducible_zeroLocus_iff_of_radical isRadical_vanishingIdeal
isIrreducible_zeroLocus_iff 📖	mathematical	—	IsIrreducible PrimeSpectrum zariskiTopology zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.IsPrime Ideal.radical	—	isIrreducible_zeroLocus_iff_of_radical Ideal.radical_isRadical zeroLocus_radical
isIrreducible_zeroLocus_iff_of_radical 📖	mathematical	Ideal.IsRadical	IsIrreducible PrimeSpectrum zariskiTopology zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.IsPrime	—	Ideal.isPrime_iff IsIrreducible.eq_1 Set.nonempty_iff_ne_empty zeroLocus_empty_iff_eq_top vanishingIdeal_zeroLocus_eq_radical Ideal.IsRadical.radical IsScalarTower.left Ideal.instIsTwoSided Ideal.IsRadical.radical_le_iff Ideal.radical_inf Ideal.radical_mul instIsConcreteLE Ideal.mul_mem_right Ideal.mul_mem_left
isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton 📖	mathematical	TopologicalSpace.Opens.carrier PrimeSpectrum zariskiTopology basicOpen Set Set.instSingletonSet	IsLocalization.Away IsLocalization.AtPrime asIdeal isPrime	—	isPrime IsLocalization.of_le_of_exists_dvd Localization.isLocalization Submonoid.powers_le Set.mem_singleton Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Ideal.exists_le_prime_disjoint Set.disjoint_right Submonoid.mem_powers Set.mem_singleton_iff Ideal.span_singleton_le_iff_mem IsLocalization.isLocalization_iff_of_isLocalization
isOpen_basicOpen 📖	mathematical	—	IsOpen PrimeSpectrum zariskiTopology SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	TopologicalSpace.Opens.isOpen
isOpen_iff 📖	mathematical	—	IsOpen PrimeSpectrum zariskiTopology Compl.compl Set Set.instCompl zeroLocus	—	—
isQuotientMap_of_generalizingMap 📖	mathematical	PrimeSpectrum comap GeneralizingMap zariskiTopology	Topology.IsQuotientMap	—	Topology.isQuotientMap_iff_isClosed IsClosed.preimage continuous_comap isClosed_image_of_stableUnderSpecialization Set.image_preimage_eq stableUnderGeneralization_compl_iff Set.preimage_compl GeneralizingMap.stableUnderGeneralization_image IsOpen.stableUnderGeneralization IsClosed.isOpen_compl
isQuotientMap_of_specializingMap 📖	mathematical	PrimeSpectrum comap SpecializingMap zariskiTopology	Topology.IsQuotientMap	—	Topology.isQuotientMap_iff_isClosed IsClosed.preimage continuous_comap isClosed_image_of_stableUnderSpecialization SpecializingMap.stableUnderSpecialization_image IsClosed.stableUnderSpecialization Set.image_preimage_eq
isRadical_vanishingIdeal 📖	mathematical	—	Ideal.IsRadical vanishingIdeal	—	vanishingIdeal_closure zeroLocus_vanishingIdeal_eq_closure vanishingIdeal_zeroLocus_eq_radical Ideal.radical_isRadical
isRetrocompact_basicOpen 📖	mathematical	—	IsRetrocompact PrimeSpectrum zariskiTopology SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	basicOpen_eq_zeroLocus_compl isRetrocompact_zeroLocus_compl Set.finite_singleton
isRetrocompact_zeroLocus_compl 📖	mathematical	—	IsRetrocompact PrimeSpectrum zariskiTopology Compl.compl Set Set.instCompl zeroLocus	—	QuasiSeparatedSpace.isRetrocompact_iff_isCompact compactSpace instQuasiSeparatedSpace IsClosed.isOpen_compl isClosed_zeroLocus isCompact_isOpen_iff Set.Finite.coe_toFinset
isRetrocompact_zeroLocus_compl_of_fg 📖	mathematical	Ideal.FG CommSemiring.toSemiring	IsRetrocompact PrimeSpectrum zariskiTopology Compl.compl Set Set.instCompl zeroLocus SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	zeroLocus_span isRetrocompact_zeroLocus_compl Finset.finite_toSet
isTopologicalBasis_basic_opens 📖	mathematical	—	TopologicalSpace.IsTopologicalBasis PrimeSpectrum zariskiTopology Set.range Set SetLike.coe TopologicalSpace.Opens TopologicalSpace.Opens.instSetLike basicOpen	—	TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen_basicOpen Set.not_subset mem_zeroLocus Set.mem_compl_iff compl_compl Set.compl_subset_compl basicOpen_eq_zeroLocus_compl zeroLocus_anti_mono Set.singleton_subset_iff
le_basicOpen_pow 📖	mathematical	—	TopologicalSpace.Opens PrimeSpectrum zariskiTopology Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder basicOpen Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	pow_zero basicOpen_one basicOpen_pow IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd
le_iff_mem_closure 📖	mathematical	—	PrimeSpectrum Preorder.toLE PartialOrder.toPreorder instPartialOrder Set Set.instMembership closure zariskiTopology Set.instSingletonSet	—	asIdeal_le_asIdeal zeroLocus_vanishingIdeal_eq_closure mem_zeroLocus vanishingIdeal_singleton SetLike.coe_subset_coe instIsConcreteLE
le_iff_specializes 📖	mathematical	—	PrimeSpectrum Preorder.toLE PartialOrder.toPreorder instPartialOrder Specializes zariskiTopology	—	le_iff_mem_closure specializes_iff_mem_closure
localization_away_comap_range 📖	mathematical	—	Set.range PrimeSpectrum comap algebraMap CommSemiring.toSemiring SetLike.coe TopologicalSpace.Opens zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen	—	localization_comap_range Set.ext basicOpen_eq_zeroLocus_compl Submonoid.mem_powers Ideal.IsPrime.mem_of_pow_mem isPrime
localization_away_isOpenEmbedding 📖	mathematical	—	Topology.IsOpenEmbedding PrimeSpectrum zariskiTopology comap algebraMap CommSemiring.toSemiring	—	localization_comap_isEmbedding localization_away_comap_range isOpen_basicOpen
localization_comap_injective 📖	mathematical	—	PrimeSpectrum comap algebraMap CommSemiring.toSemiring	—	ext RingHom.instRingHomClass IsLocalization.map_comap
localization_comap_isEmbedding 📖	mathematical	—	Topology.IsEmbedding PrimeSpectrum zariskiTopology comap algebraMap CommSemiring.toSemiring	—	localization_comap_isInducing localization_comap_injective
localization_comap_isInducing 📖	mathematical	—	Topology.IsInducing PrimeSpectrum zariskiTopology comap algebraMap CommSemiring.toSemiring	—	TopologicalSpace.ext_isClosed preimage_comap_zeroLocus RingHom.instRingHomClass zeroLocus_span Ideal.map.eq_1 IsLocalization.map_comap
localization_comap_range 📖	mathematical	—	Set.range PrimeSpectrum comap algebraMap CommSemiring.toSemiring setOf Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Submonoid.instSetLike Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule asIdeal	—	Set.ext RingHom.instRingHomClass IsLocalization.isPrime_iff_isPrime_disjoint isPrime IsLocalization.isPrime_of_isPrime_disjoint ext IsLocalization.comap_map_of_isPrime_disjoint
localization_specComap_injective 📖	mathematical	—	PrimeSpectrum comap algebraMap CommSemiring.toSemiring	—	localization_comap_injective
localization_specComap_range 📖	mathematical	—	Set.range PrimeSpectrum comap algebraMap CommSemiring.toSemiring setOf Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Submonoid.instSetLike Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule asIdeal	—	localization_comap_range
maximalSpectrumToPiLocalization_surjective_of_discreteTopology 📖	mathematical	—	MaximalSpectrum.PiLocalization DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.nonAssocSemiring MaximalSpectrum Localization.AtPrime MaximalSpectrum.asIdeal OreLocalization.instSemiring Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid RingHom.instFunLike MaximalSpectrum.toPiLocalization	—	isPrime piLocalizationToMaximal_comp_toPiLocalization piLocalizationToMaximal_surjective toPiLocalization_surjective_of_discreteTopology
mem_basicOpen 📖	mathematical	—	PrimeSpectrum TopologicalSpace.Opens zariskiTopology SetLike.instMembership TopologicalSpace.Opens.instSetLike basicOpen Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	—
nhdsOrderEmbedding_apply 📖	mathematical	—	DFunLike.coe RelEmbedding PrimeSpectrum Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder Filter.instPartialOrder RelEmbedding.instFunLike nhdsOrderEmbedding nhds zariskiTopology	—	—
primeSpectrumProd_symm_inl 📖	mathematical	—	DFunLike.coe Equiv PrimeSpectrum Prod.instCommSemiring EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primeSpectrumProd comap RingHom.fst Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	ext Ideal.ext primeSpectrumProd_symm_inl_asIdeal Ideal.comap_top inf_of_le_left RingHom.instRingHomClass
primeSpectrumProd_symm_inr 📖	mathematical	—	DFunLike.coe Equiv PrimeSpectrum Prod.instCommSemiring EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primeSpectrumProd comap RingHom.snd Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	ext Ideal.ext primeSpectrumProd_symm_inr_asIdeal Ideal.comap_top inf_of_le_right RingHom.instRingHomClass
quasiSober 📖	mathematical	—	QuasiSober PrimeSpectrum zariskiTopology	—	isIrreducible_iff_vanishingIdeal_isPrime IsGenericPoint.eq_1 closure_singleton zeroLocus_vanishingIdeal_eq_closure IsClosed.closure_eq
range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk 📖	mathematical	—	Compl.compl Set PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring Set.instCompl Set.range Localization.Away CommRing.toCommMonoid OreLocalization.instSemiring Ring.toSemiring CommRing.toRing Submonoid.powers CommMonoid.toMonoid OreLocalization.oreSetComm OreLocalization.instCommSemiring comap algebraMap Polynomial.semiring RingHom.toAlgebra Polynomial.mapRingHom OreLocalization.instAlgebra Algebra.id HasQuotient.Quotient Ideal Ideal.instHasQuotient Ideal.span Set.instSingletonSet Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.Quotient.commSemiring	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.isLocalization Localization.isLocalization Ideal.instIsTwoSided_1 Polynomial.map_surjective Ideal.Quotient.mk_surjective range_comap_of_surjective localization_away_comap_range Submonoid.map_powers basicOpen_eq_zeroLocus_compl compl_compl Polynomial.ker_mapRingHom Ideal.mk_ker Ideal.map_span Set.image_singleton zeroLocus_span
range_comap_fst 📖	mathematical	—	Set.range PrimeSpectrum Prod.instCommSemiring comap RingHom.fst Semiring.toNonAssocSemiring CommSemiring.toSemiring zeroLocus SetLike.coe Ideal Prod.instSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.ker RingHom Prod.instNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass	—	Set.ext RingHom.instRingHomClass Ideal.comap_mono bot_le Ideal.ideal_prod_prime isPrime ext Ideal.comap_top inf_of_le_left Ideal.IsPrime.ne_top Ideal.eq_top_iff_one
range_comap_snd 📖	mathematical	—	Set.range PrimeSpectrum Prod.instCommSemiring comap RingHom.snd Semiring.toNonAssocSemiring CommSemiring.toSemiring zeroLocus SetLike.coe Ideal Prod.instSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.ker RingHom Prod.instNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass	—	Set.ext RingHom.instRingHomClass Ideal.comap_mono bot_le Ideal.ideal_prod_prime isPrime Ideal.IsPrime.ne_top Ideal.eq_top_iff_one ext Ideal.comap_top inf_of_le_right
stableUnderGeneralization_singleton 📖	mathematical	—	StableUnderGeneralization PrimeSpectrum zariskiTopology Set Set.instSingletonSet Ideal CommSemiring.toSemiring Set.instMembership minimalPrimes asIdeal	—	Eq.ge le_antisymm
stableUnderSpecialization_image_iff 📖	mathematical	—	StableUnderSpecialization PrimeSpectrum zariskiTopology Set.image comap IsClosed	—	isClosed_image_of_stableUnderSpecialization IsClosed.stableUnderSpecialization
stableUnderSpecialization_range_iff 📖	mathematical	—	StableUnderSpecialization PrimeSpectrum zariskiTopology Set.range comap IsClosed	—	isClosed_range_of_stableUnderSpecialization IsClosed.stableUnderSpecialization
stableUnderSpecialization_singleton 📖	mathematical	—	StableUnderSpecialization PrimeSpectrum zariskiTopology Set Set.instSingletonSet Ideal.IsMaximal CommSemiring.toSemiring asIdeal	—	Eq.le le_antisymm
t1Space_iff_isField 📖	mathematical	—	T1Space PrimeSpectrum zariskiTopology IsField CommSemiring.toSemiring	—	Ideal.isPrime_bot IsDomain.toNontrivial IsDomain.to_noZeroDivisors Ring.ne_bot_of_isMaximal_of_not_isField isClosed_singleton_iff_isMaximal T1Space.t1 Ideal.bot_isMaximal Ring.not_isField_iff_exists_prime isPrime
toPiLocalization_bijective 📖	mathematical	—	Function.Bijective PiLocalization CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.nonAssocSemiring PrimeSpectrum Localization CommSemiring.toCommMonoid Ideal.primeCompl asIdeal isPrime OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.instFunLike toPiLocalization	—	isPrime discreteTopology_iff_toPiLocalization_bijective
toPiLocalization_surjective_of_discreteTopology 📖	mathematical	—	PiLocalization DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Pi.nonAssocSemiring PrimeSpectrum Localization CommSemiring.toCommMonoid Ideal.primeCompl asIdeal isPrime OreLocalization.instSemiring OreLocalization.oreSetComm RingHom.instFunLike toPiLocalization	—	TopologicalSpace.IsTopologicalBasis.isOpen_iff isTopologicalBasis_basic_opens isOpen_discrete HasSubset.Subset.antisymm Set.instAntisymmSubset Set.singleton_subset_iff Set.singleton_injective isPrime isLocalization_away_iff_atPrime_of_basicOpen_eq_singleton Equiv.apply_ofInjective_symm Localization.isLocalization iSup_basicOpen_eq_top_iff top_unique TopologicalSpace.Opens.mem_iSup Eq.ge Localization.existsUnique_algebraMap_eq_of_span_eq_top eq_or_ne basicOpen_eq_bot_iff basicOpen_mul bot_unique Equiv.injective IsLocalization.subsingleton Equiv.symm_apply_apply AlgEquiv.commutes AlgEquiv.symm_apply_eq
topologicalKrullDim_eq_ringKrullDim 📖	mathematical	—	topologicalKrullDim PrimeSpectrum zariskiTopology ringKrullDim	—	Order.krullDim_orderDual Order.krullDim_eq_of_orderIso
vanishingIdeal_anti_mono_iff 📖	mathematical	—	Set PrimeSpectrum Set.instHasSubset Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal	—	vanishingIdeal_anti_mono IsClosed.closure_subset_iff IsClosed.closure_eq zeroLocus_vanishingIdeal_eq_closure zeroLocus_anti_mono_ideal
vanishingIdeal_closure 📖	mathematical	—	vanishingIdeal closure PrimeSpectrum zariskiTopology	—	GaloisConnection.u_l_u_eq_u gc zeroLocus_vanishingIdeal_eq_closure
vanishingIdeal_irreducibleComponents 📖	mathematical	—	Set.image Set PrimeSpectrum Ideal CommSemiring.toSemiring vanishingIdeal irreducibleComponents zariskiTopology minimalPrimes	—	irreducibleComponents_eq_maximals_closed minimalPrimes_eq_minimals image_antitone_setOf_maximal vanishingIdeal_anti_mono_iff Set.mem_setOf_eq vanishingIdeal_isClosed_isIrreducible
vanishingIdeal_isClosed_isIrreducible 📖	mathematical	—	Set.image Set PrimeSpectrum Ideal CommSemiring.toSemiring vanishingIdeal setOf IsClosed zariskiTopology IsIrreducible Ideal.IsPrime	—	subset_antisymm Set.instAntisymmSubset Set.image_mono isClosed_closure IsIrreducible.closure vanishingIdeal_closure vanishingIdeal_isIrreducible
vanishingIdeal_isIrreducible 📖	mathematical	—	Set.image Set PrimeSpectrum Ideal CommSemiring.toSemiring vanishingIdeal setOf IsIrreducible zariskiTopology Ideal.IsPrime	—	Set.ext isIrreducible_iff_vanishingIdeal_isPrime isIrreducible_zeroLocus_iff_of_radical Ideal.IsPrime.isRadical vanishingIdeal_zeroLocus_eq_radical Ideal.IsPrime.radical
vanishingIdeal_mem_minimalPrimes 📖	mathematical	—	Ideal CommSemiring.toSemiring Set Set.instMembership minimalPrimes vanishingIdeal PrimeSpectrum irreducibleComponents zariskiTopology closure	—	zeroLocus_minimalPrimes zeroLocus_vanishingIdeal_eq_closure Set.mem_image_of_mem vanishingIdeal_irreducibleComponents vanishingIdeal_closure
vanishingIdeal_range_comap 📖	mathematical	—	vanishingIdeal Set.range PrimeSpectrum comap Ideal.radical RingHom.ker RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike RingHom.instRingHomClass	—	Ideal.ext RingHom.instRingHomClass RingHom.ker_eq_comap_bot Ideal.comap_radical Ideal.radical_eq_sInf Ideal.comap.congr_simp isPrime
vanishingIdeal_strict_anti_mono_iff 📖	mathematical	—	Set PrimeSpectrum Set.instHasSSubset Ideal CommSemiring.toSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal	—	Set.ssubset_def vanishingIdeal_anti_mono_iff lt_iff_le_not_ge
zeroLocus_eq_basicOpen_of_isIdempotentElem 📖	mathematical	IsIdempotentElem Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	zeroLocus CommRing.toCommSemiring Set Set.instSingletonSet SetLike.coe TopologicalSpace.Opens PrimeSpectrum zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	basicOpen_eq_zeroLocus_of_isIdempotentElem IsIdempotentElem.one_sub sub_sub_cancel
zeroLocus_eq_basicOpen_of_mul_add 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	zeroLocus Set Set.instSingletonSet SetLike.coe TopologicalSpace.Opens PrimeSpectrum zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen	—	basicOpen_eq_zeroLocus_of_mul_add mul_comm add_comm
zeroLocus_eq_iff 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.radical	—	zeroLocus_radical
zeroLocus_ideal_mem_irreducibleComponents 📖	mathematical	—	Set PrimeSpectrum Set.instMembership irreducibleComponents zariskiTopology zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule minimalPrimes Ideal.radical	—	vanishingIdeal_zeroLocus_eq_radical IsClosed.closure_eq isClosed_zeroLocus vanishingIdeal_mem_minimalPrimes
zeroLocus_minimalPrimes 📖	mathematical	—	Set.image Ideal CommSemiring.toSemiring Set PrimeSpectrum zeroLocus SetLike.coe Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule minimalPrimes irreducibleComponents zariskiTopology	—	vanishingIdeal_irreducibleComponents Set.image_comp Set.EqOn.image_eq_self zeroLocus_vanishingIdeal_eq_closure isClosed_of_mem_irreducibleComponents
zeroLocus_vanishingIdeal_eq_closure 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal closure PrimeSpectrum zariskiTopology	—	isClosed_iff_zeroLocus isClosed_closure subset_antisymm_iff Set.instReflSubset Set.instAntisymmSubset IsClosed.closure_subset_iff isClosed_zeroLocus subset_zeroLocus_iff_subset_vanishingIdeal GaloisConnection.u_l_u_eq_u gc subset_closure subset_zeroLocus_vanishingIdeal

RingHom.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_surjective 📖	mathematical	RingHom.IsIntegral CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	PrimeSpectrum PrimeSpectrum.comap	—	RingHom.instRingHomClass Ideal.exists_ideal_over_prime_of_isIntegral Ideal.comap_bot_of_injective
specComap_surjective 📖	mathematical	RingHom.IsIntegral CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	PrimeSpectrum PrimeSpectrum.comap	—	comap_surjective

minimalPrimes

Definitions

Name	Category	Theorems
equivIrreducibleComponents 📖	CompOp	—

---

← Back to Index