Basic

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

Statistics

Metric	Count
Definitions instOrderBotOfIsDomain, instUnique, primeSpectrumProd, primeSpectrumProdOfSum, vanishingIdeal, zeroLocus	6
Theorems asIdeal_bot, coe_vanishingIdeal, exists_primeSpectrum_prod_le, exists_primeSpectrum_prod_le_and_ne_bot_of_domain, gc, gc_set, instIsEmptyOfSubsingleton, instNonemptyOfNontrivial, isEmpty_iff_subsingleton, isMax_iff, isMin_iff, le_vanishingIdeal_zeroLocus, mem_compl_zeroLocus_iff_notMem, mem_vanishingIdeal, mem_zeroLocus, nilradical_eq_iInf, nonempty_iff_nontrivial, nontrivial, primeSpectrumProd_symm_inl_asIdeal, primeSpectrumProd_symm_inr_asIdeal, range_asIdeal, subset_vanishingIdeal_zeroLocus, subset_zeroLocus_iff_le_vanishingIdeal, subset_zeroLocus_iff_subset_vanishingIdeal, subset_zeroLocus_vanishingIdeal, sup_vanishingIdeal_le, union_zeroLocus, vanishingIdeal_anti_mono, vanishingIdeal_empty, vanishingIdeal_eq_top_iff, vanishingIdeal_iUnion, vanishingIdeal_singleton, vanishingIdeal_union, vanishingIdeal_univ, vanishingIdeal_zeroLocus_eq_radical, zeroLocus_anti_mono, zeroLocus_anti_mono_ideal, zeroLocus_bUnion, zeroLocus_bot, zeroLocus_diff_singleton_zero, zeroLocus_empty, zeroLocus_empty_iff_eq_top, zeroLocus_empty_of_one_mem, zeroLocus_eq_singleton, zeroLocus_eq_univ_iff, zeroLocus_iSup, zeroLocus_iUnion, zeroLocus_iUnion₂, zeroLocus_inf, zeroLocus_insert_zero, zeroLocus_mul, zeroLocus_nilradical, zeroLocus_pow, zeroLocus_radical, zeroLocus_singleton_mul, zeroLocus_singleton_one, zeroLocus_singleton_pow, zeroLocus_singleton_zero, zeroLocus_smul_of_isUnit, zeroLocus_span, zeroLocus_subset_zeroLocus_iff, zeroLocus_subset_zeroLocus_singleton_iff, zeroLocus_sup, zeroLocus_union, zeroLocus_univ	65
Total	71

PrimeSpectrum

Definitions

Name	Category	Theorems
instOrderBotOfIsDomain 📖	CompOp	3 math math: asIdeal_bot, IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top, AlgebraicGeometry.genericPoint_eq_bot_of_affine
instUnique 📖	CompOp	—
primeSpectrumProd 📖	CompOp	6 math math: AlgebraicGeometry.coprodSpec_apply, primeSpectrumProd_symm_inl, primeSpectrumProd_symm_inr_asIdeal, primeSpectrumProd_symm_inr, AlgebraicGeometry.coprodSpec_coprodMk, primeSpectrumProd_symm_inl_asIdeal
primeSpectrumProdOfSum 📖	CompOp	—
vanishingIdeal 📖	CompOp	31 math math: vanishingIdeal_isClosed_isIrreducible, gc, vanishingIdeal_strict_anti_mono_iff, vanishingIdeal_zeroLocus_eq_radical, vanishingIdeal_range_comap, vanishingIdeal_irreducibleComponents, vanishingIdeal_anti_mono_iff, vanishingIdeal_eq_top_iff, MvPolynomial.vanishingIdeal_pointToPoint, sup_vanishingIdeal_le, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, subset_vanishingIdeal_zeroLocus, vanishingIdeal_isIrreducible, subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_anti_mono, isRadical_vanishingIdeal, vanishingIdeal_union, vanishingIdeal_empty, vanishingIdeal_singleton, gc_set, vanishingIdeal_univ, coe_vanishingIdeal, subset_zeroLocus_vanishingIdeal, mem_vanishingIdeal, isIrreducible_iff_vanishingIdeal_isPrime, vanishingIdeal_closure, subset_zeroLocus_iff_subset_vanishingIdeal, vanishingIdeal_iUnion, vanishingIdeal_mem_minimalPrimes, le_vanishingIdeal_zeroLocus, zeroLocus_vanishingIdeal_eq_closure
zeroLocus 📖	CompOp	104 math math: zeroLocus_anti_mono, closure_range_comap, Module.support_quotient, isClosed_zeroLocus, zeroLocus_nilradical, isClopen_iff_mul_add_zeroLocus, zeroLocus_eq_univ_iff, zeroLocus_empty, range_comap_of_surjective, isRetrocompact_zeroLocus_compl_of_fg, gc, MvPolynomial.image_comap_C_basicOpen, isClosed_iff_zeroLocus, range_specComap_of_surjective, basicOpen_eq_zeroLocus_of_mul_add, instQuasiSoberElemZeroLocus, ringKrullDim_quotient, vanishingIdeal_zeroLocus_eq_radical, AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, isCompact_isOpen_iff, union_zeroLocus, zeroLocus_diff_singleton_zero, zeroLocus_subset_zeroLocus_iff, zeroLocus_span, isClosed_iff_zeroLocus_radical_ideal, basicOpen_eq_zeroLocus_of_isIdempotentElem, zeroLocus_eq_basicOpen_of_isIdempotentElem, AlgebraicGeometry.Scheme.isoSpec_inv_image_zeroLocus, isIrreducible_zeroLocus_iff_of_radical, preimage_comap_zeroLocus, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, mem_compl_zeroLocus_iff_notMem, zeroLocus_radical, zeroLocus_minimalPrimes, isIrreducible_zeroLocus_iff, Polynomial.exists_image_comap_of_monic, Polynomial.isOpen_image_comap_of_monic, AlgebraicGeometry.Polynomial.imageOfDf_eq_comap_C_compl_zeroLocus, zeroLocus_insert_zero, Module.support_of_algebra, mem_zeroLocus, preimage_specComap_zeroLocus, zeroLocus_subset_zeroLocus_singleton_iff, subset_vanishingIdeal_zeroLocus, zeroLocus_union, subset_zeroLocus_iff_le_vanishingIdeal, zeroLocus_bUnion, zeroLocus_ideal_mem_irreducibleComponents, zeroLocus_iSup, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus, image_comap_zeroLocus_eq_zeroLocus_comap, zeroLocus_eq_iff, isOpen_iff, MvPolynomial.pointToPoint_zeroLocus_le, isClosed_iff_zeroLocus_ideal, Polynomial.isCompact_image_comap_of_monic, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, zeroLocus_bot, range_comap_snd, zeroLocus_iUnion, zeroLocus_mul, AlgebraicGeometry.Scheme.toSpecΓ_image_zeroLocus, preimage_comap_zeroLocus_aux, zeroLocus_smul_of_isUnit, closure_image_comap_zeroLocus, closure_singleton, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, Polynomial.image_comap_C_basicOpen, gc_set, Module.support_quotSMulTop, isRetrocompact_zeroLocus_compl, LocalizedModule.subsingleton_iff_support_subset, AlgebraicGeometry.Spec_zeroLocus, zeroLocus_univ, support_of_supportDim_eq_zero, zeroLocus_iUnion₂, zeroLocus_singleton_pow, image_specComap_zeroLocus_eq_zeroLocus_comap, basicOpen_eq_zeroLocus_compl, zeroLocus_empty_of_one_mem, Module.support_eq_zeroLocus, zeroLocus_singleton_one, subset_zeroLocus_vanishingIdeal, zeroLocus_singleton_mul, isClopen_iff_zeroLocus, zeroLocus_inf, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, exists_image_comap_of_finite_of_free, zeroLocus_eq_basicOpen_of_mul_add, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq, zeroLocus_sup, mem_image_comap_zeroLocus_sdiff, range_comap_fst, zeroLocus_empty_iff_eq_top, zeroLocus_anti_mono_ideal, zeroLocus_singleton_zero, AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus, subset_zeroLocus_iff_subset_vanishingIdeal, isCompact_isOpen_iff_ideal, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_zeroLocus, zeroLocus_pow, le_vanishingIdeal_zeroLocus, zeroLocus_vanishingIdeal_eq_closure, zeroLocus_eq_singleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asIdeal_bot 📖	mathematical	—	asIdeal Bot.bot PrimeSpectrum OrderBot.toBot Preorder.toLE PartialOrder.toPreorder instPartialOrder instOrderBotOfIsDomain Ideal CommSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
coe_vanishingIdeal 📖	mathematical	—	SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal setOf	—	Set.ext vanishingIdeal.eq_1 SetLike.mem_coe Submodule.mem_iInf
exists_primeSpectrum_prod_le 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Multiset.prod CommSemiring.toCommMonoid IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Multiset.map PrimeSpectrum asIdeal	—	IsNoetherian.induction Multiset.map_singleton Multiset.prod_singleton le_refl le_top lt_of_le_of_ne le_sup_left Ideal.mem_sup_right Submodule.mem_span_singleton_self Ideal.not_isPrime_iff Multiset.map_add Multiset.prod_add le_trans IsScalarTower.right mul_le_mul' Submodule.instMulLeftMono Submodule.instMulRightMono add_mul Distrib.rightDistribClass sup_le Ideal.mul_le_right Ideal.instIsTwoSided_1 mul_add Distrib.leftDistribClass Ideal.mul_le_left Submodule.span_mul_span Set.singleton_mul_singleton Submodule.span_singleton_le_iff_mem
exists_primeSpectrum_prod_le_and_ne_bot_of_domain 📖	mathematical	IsField CommSemiring.toSemiring CommRing.toCommSemiring	Ideal Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Multiset.prod CommSemiring.toCommMonoid IdemCommSemiring.toCommSemiring Ideal.instIdemCommSemiring Multiset.map PrimeSpectrum asIdeal	—	IsNoetherian.induction IsDomain.toNontrivial Ring.not_isField_iff_exists_prime le_top Multiset.map_singleton Multiset.prod_singleton le_rfl Ideal.not_isPrime_iff lt_of_le_of_ne le_sup_left Submodule.mem_sup_right Submodule.mem_span_singleton_self ne_bot_of_gt Multiset.map_add Multiset.prod_add le_trans mul_le_mul' Submodule.instMulLeftMono IsScalarTower.right Submodule.instMulRightMono add_mul Distrib.rightDistribClass sup_le Ideal.mul_le_right Ideal.instIsTwoSided_1 mul_add Distrib.leftDistribClass Ideal.mul_le_left Submodule.span_mul_span Set.singleton_mul_singleton Submodule.span_singleton_le_iff_mem IsScalarTower.left Ideal.mul_eq_bot IsDomain.to_noZeroDivisors
gc 📖	mathematical	—	GaloisConnection Ideal CommSemiring.toSemiring OrderDual Set PrimeSpectrum PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule OrderDual.instPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra zeroLocus SetLike.coe Submodule.setLike vanishingIdeal	—	subset_zeroLocus_iff_le_vanishingIdeal
gc_set 📖	mathematical	—	GaloisConnection Set OrderDual PrimeSpectrum PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra OrderDual.instPreorder zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal	—	GaloisInsertion.gc zeroLocus_span GaloisConnection.compose gc
instIsEmptyOfSubsingleton 📖	mathematical	—	IsEmpty PrimeSpectrum	—	isEmpty_iff_subsingleton
instNonemptyOfNontrivial 📖	mathematical	—	PrimeSpectrum	—	nonempty_iff_nontrivial
isEmpty_iff_subsingleton 📖	mathematical	—	IsEmpty PrimeSpectrum	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ nonempty_iff_nontrivial
isMax_iff 📖	mathematical	—	IsMax PrimeSpectrum Preorder.toLE PartialOrder.toPreorder instPartialOrder Ideal.IsMaximal CommSemiring.toSemiring asIdeal	—	Ideal.IsPrime.ne_top isPrime Ideal.exists_le_maximal IsMax.not_lt Ideal.IsMaximal.isPrime LT.lt.trans_le Eq.ge Ideal.IsMaximal.eq_of_le
isMin_iff 📖	mathematical	—	IsMin PrimeSpectrum Preorder.toLE PartialOrder.toPreorder instPartialOrder Ideal CommSemiring.toSemiring Set Set.instMembership minimalPrimes asIdeal	—	isPrime
le_vanishingIdeal_zeroLocus 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal zeroLocus SetLike.coe Submodule.setLike	—	GaloisConnection.le_u_l gc
mem_compl_zeroLocus_iff_notMem 📖	mathematical	—	PrimeSpectrum Set Set.instMembership Compl.compl Set.instCompl zeroLocus Set.instSingletonSet Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	Set.mem_compl_iff mem_zeroLocus Set.singleton_subset_iff
mem_vanishingIdeal 📖	mathematical	—	Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal asIdeal	—	SetLike.mem_coe coe_vanishingIdeal Set.mem_setOf_eq
mem_zeroLocus 📖	mathematical	—	PrimeSpectrum Set Set.instMembership zeroLocus Set.instHasSubset SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	—
nilradical_eq_iInf 📖	mathematical	—	nilradical iInf Ideal CommSemiring.toSemiring PrimeSpectrum Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	nilradical_eq_sInf range_asIdeal
nonempty_iff_nontrivial 📖	mathematical	—	PrimeSpectrum Nontrivial	—	Ideal.IsPrime.ne_top isPrime Ideal.eq_top_iff_one AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Ideal.exists_maximal Ideal.IsMaximal.isPrime
nontrivial 📖	mathematical	—	Nontrivial	—	nonempty_iff_nontrivial
primeSpectrumProd_symm_inl_asIdeal 📖	mathematical	—	asIdeal Prod.instCommSemiring DFunLike.coe Equiv PrimeSpectrum EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primeSpectrumProd Ideal.prod CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
primeSpectrumProd_symm_inr_asIdeal 📖	mathematical	—	asIdeal Prod.instCommSemiring DFunLike.coe Equiv PrimeSpectrum EquivLike.toFunLike Equiv.instEquivLike Equiv.symm primeSpectrumProd Ideal.prod CommSemiring.toSemiring Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
range_asIdeal 📖	mathematical	—	Set.range Ideal CommSemiring.toSemiring PrimeSpectrum asIdeal setOf Ideal.IsPrime	—	Set.ext Set.mem_range Set.mem_setOf isPrime
subset_vanishingIdeal_zeroLocus 📖	mathematical	—	Set Set.instHasSubset SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal zeroLocus	—	GaloisConnection.le_u_l gc_set
subset_zeroLocus_iff_le_vanishingIdeal 📖	mathematical	—	Set PrimeSpectrum Set.instHasSubset zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder vanishingIdeal	—	mem_vanishingIdeal mem_zeroLocus le_trans
subset_zeroLocus_iff_subset_vanishingIdeal 📖	mathematical	—	Set PrimeSpectrum Set.instHasSubset zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal	—	gc_set
subset_zeroLocus_vanishingIdeal 📖	mathematical	—	Set PrimeSpectrum Set.instHasSubset zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal	—	GaloisConnection.l_u_le gc
sup_vanishingIdeal_le 📖	mathematical	—	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id vanishingIdeal Set PrimeSpectrum Set.instInter	—	Submodule.mem_sup mem_vanishingIdeal Submodule.add_mem
union_zeroLocus 📖	mathematical	—	Set PrimeSpectrum Set.instUnion zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instMin Ideal.span	—	zeroLocus_inf zeroLocus_span
vanishingIdeal_anti_mono 📖	mathematical	Set PrimeSpectrum Set.instHasSubset	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule vanishingIdeal	—	GaloisConnection.monotone_u gc
vanishingIdeal_empty 📖	mathematical	—	vanishingIdeal Set PrimeSpectrum Set.instEmptyCollection Top.top Ideal CommSemiring.toSemiring Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	GaloisConnection.u_top gc
vanishingIdeal_eq_top_iff 📖	mathematical	—	vanishingIdeal Top.top Ideal CommSemiring.toSemiring Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set PrimeSpectrum Set.instEmptyCollection	—	top_le_iff subset_zeroLocus_iff_le_vanishingIdeal Submodule.top_coe zeroLocus_univ Set.subset_empty_iff
vanishingIdeal_iUnion 📖	mathematical	—	vanishingIdeal Set.iUnion PrimeSpectrum iInf Ideal CommSemiring.toSemiring Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	GaloisConnection.u_iInf gc
vanishingIdeal_singleton 📖	mathematical	—	vanishingIdeal PrimeSpectrum Set Set.instSingletonSet asIdeal	—	iInf_congr_Prop iInf_iInf_eq_left
vanishingIdeal_union 📖	mathematical	—	vanishingIdeal Set PrimeSpectrum Set.instUnion Ideal CommSemiring.toSemiring Submodule.instMin NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	GaloisConnection.u_inf gc
vanishingIdeal_univ 📖	mathematical	—	vanishingIdeal Set.univ PrimeSpectrum nilradical	—	vanishingIdeal.eq_1 iInf_univ nilradical_eq_iInf
vanishingIdeal_zeroLocus_eq_radical 📖	mathematical	—	vanishingIdeal zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.radical	—	Ideal.ext mem_vanishingIdeal Ideal.radical_eq_sInf Submodule.mem_sInf isPrime
zeroLocus_anti_mono 📖	mathematical	Set Set.instHasSubset	PrimeSpectrum zeroLocus	—	GaloisConnection.monotone_l gc_set
zeroLocus_anti_mono_ideal 📖	mathematical	Ideal CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Set PrimeSpectrum Set.instHasSubset zeroLocus SetLike.coe Submodule.setLike	—	GaloisConnection.monotone_l gc
zeroLocus_bUnion 📖	mathematical	—	zeroLocus Set.iUnion Set Set.instMembership Set.iInter PrimeSpectrum	—	zeroLocus_iUnion
zeroLocus_bot 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Bot.bot Submodule.instBot Set.univ PrimeSpectrum	—	GaloisConnection.l_bot gc
zeroLocus_diff_singleton_zero 📖	mathematical	—	zeroLocus Set Set.instSDiff Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	zeroLocus_insert_zero Set.insert_diff_singleton
zeroLocus_empty 📖	mathematical	—	zeroLocus Set Set.instEmptyCollection Set.univ PrimeSpectrum	—	GaloisConnection.l_bot gc_set
zeroLocus_empty_iff_eq_top 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set PrimeSpectrum Set.instEmptyCollection Top.top Submodule.instTop	—	Mathlib.Tactic.Contrapose.contrapose₁ Ideal.exists_le_maximal Ideal.IsMaximal.isPrime zeroLocus_empty_of_one_mem
zeroLocus_empty_of_one_mem 📖	mathematical	Set Set.instMembership AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	zeroLocus PrimeSpectrum Set.instEmptyCollection	—	Set.eq_empty_iff_forall_notMem isPrime Ideal.eq_top_iff_one mem_zeroLocus Ideal.IsPrime.ne_top
zeroLocus_eq_singleton 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum Set Set.instSingletonSet Ideal.IsPrime Ideal.IsMaximal.isPrime'	—	Set.ext Ideal.IsMaximal.isPrime' ext_iff Ideal.IsMaximal.eq_of_le Ideal.IsPrime.ne_top isPrime instIsConcreteLE Set.mem_singleton_iff Set.instReflSubset
zeroLocus_eq_univ_iff 📖	mathematical	—	zeroLocus Set.univ PrimeSpectrum Set Set.instHasSubset SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule nilradical	—	Set.univ_subset_iff subset_zeroLocus_iff_subset_vanishingIdeal vanishingIdeal_univ
zeroLocus_iSup 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set.iInter PrimeSpectrum	—	GaloisConnection.l_iSup gc
zeroLocus_iUnion 📖	mathematical	—	zeroLocus Set.iUnion Set.iInter PrimeSpectrum	—	GaloisConnection.l_iSup gc_set
zeroLocus_iUnion₂ 📖	mathematical	—	zeroLocus Set.iUnion Set.iInter PrimeSpectrum	—	GaloisConnection.l_iSup₂ gc_set
zeroLocus_inf 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instMin Set PrimeSpectrum Set.instUnion	—	Set.ext Ideal.IsPrime.inf_le isPrime
zeroLocus_insert_zero 📖	mathematical	—	zeroLocus Set Set.instInsert MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Set.union_singleton zeroLocus_union zeroLocus_singleton_zero Set.inter_univ
zeroLocus_mul 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.mul IsScalarTower.right Algebra.id Set PrimeSpectrum Set.instUnion	—	Set.ext IsScalarTower.right Ideal.IsPrime.mul_le isPrime
zeroLocus_nilradical 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule nilradical Set.univ PrimeSpectrum	—	nilradical.eq_1 zeroLocus_radical Ideal.zero_eq_bot zeroLocus_bot
zeroLocus_pow 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id	—	IsScalarTower.right zeroLocus_radical Ideal.radical_pow
zeroLocus_radical 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.radical	—	GaloisConnection.l_u_l_eq_l gc vanishingIdeal_zeroLocus_eq_radical
zeroLocus_singleton_mul 📖	mathematical	—	zeroLocus Set Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring PrimeSpectrum Set.instUnion	—	Set.ext Ideal.IsPrime.mul_mem_iff_mem_or_mem Ideal.instIsTwoSided isPrime
zeroLocus_singleton_one 📖	mathematical	—	zeroLocus Set Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring PrimeSpectrum Set.instEmptyCollection	—	zeroLocus_empty_of_one_mem Set.mem_singleton
zeroLocus_singleton_pow 📖	mathematical	—	zeroLocus Set Set.instSingletonSet Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	—	Set.ext Ideal.IsPrime.pow_mem_iff_mem isPrime
zeroLocus_singleton_zero 📖	mathematical	—	zeroLocus Set Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Set.univ PrimeSpectrum	—	zeroLocus_bot
zeroLocus_smul_of_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	zeroLocus Set Set.smulSet Algebra.toSMul Algebra.id	—	Set.ext Set.image_congr Ideal.unit_mul_mem_iff_mem
zeroLocus_span 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.span	—	Set.ext GaloisInsertion.gc
zeroLocus_subset_zeroLocus_iff 📖	mathematical	—	Set PrimeSpectrum Set.instHasSubset zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Ideal.radical	—	subset_zeroLocus_iff_le_vanishingIdeal vanishingIdeal_zeroLocus_eq_radical
zeroLocus_subset_zeroLocus_singleton_iff 📖	mathematical	—	Set PrimeSpectrum Set.instHasSubset zeroLocus Set.instSingletonSet Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.radical Ideal.span	—	zeroLocus_span zeroLocus_subset_zeroLocus_iff Ideal.span_le Set.singleton_subset_iff SetLike.mem_coe
zeroLocus_sup 📖	mathematical	—	zeroLocus SetLike.coe Ideal CommSemiring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id Set PrimeSpectrum Set.instInter	—	GaloisConnection.l_sup gc
zeroLocus_union 📖	mathematical	—	zeroLocus Set Set.instUnion PrimeSpectrum Set.instInter	—	GaloisConnection.l_sup gc_set
zeroLocus_univ 📖	mathematical	—	zeroLocus Set.univ Set PrimeSpectrum Set.instEmptyCollection	—	zeroLocus_empty_of_one_mem Set.mem_univ

---

← Back to Index