Nullstellensatz

📁 Source: Mathlib/RingTheory/Nullstellensatz.lean

Statistics

Metric	Count
Definitions `pointToPoint`, `vanishingIdeal`, `zeroLocus`	3
Theorems `vanishingIdeal_zeroLocus`, `eq_vanishingIdeal_singleton_of_isMaximal`, `instIsMaximalVanishingIdealSingletonForallSet`, `instIsPrimeVanishingIdealSingletonForallSet`, `isMaximal_iff_eq_vanishingIdeal_singleton`, `le_vanishingIdeal_zeroLocus`, `le_zeroLocus_iff_le_vanishingIdeal`, `mem_vanishingIdeal_iff`, `mem_vanishingIdeal_singleton_iff`, `mem_zeroLocus_iff`, `pointToPoint_zeroLocus_le`, `radical_le_vanishingIdeal_zeroLocus`, `vanishingIdeal_anti_mono`, `vanishingIdeal_empty`, `vanishingIdeal_pointToPoint`, `vanishingIdeal_zeroLocus_eq_radical`, `zeroLocus_anti_mono`, `zeroLocus_bot`, `zeroLocus_span`, `zeroLocus_top`, `zeroLocus_vanishingIdeal_galoisConnection`, `zeroLocus_vanishingIdeal_le`	22
Total	25

MvPolynomial

Definitions

Name	Category	Theorems
`pointToPoint` 📖	CompOp	2 math math: `vanishingIdeal_pointToPoint`, `pointToPoint_zeroLocus_le`
`vanishingIdeal` 📖	CompOp	16 math math: `vanishingIdeal_anti_mono`, `radical_le_vanishingIdeal_zeroLocus`, `le_vanishingIdeal_zeroLocus`, `zeroLocus_vanishingIdeal_le`, `IsPrime.vanishingIdeal_zeroLocus`, `vanishingIdeal_pointToPoint`, `instIsPrimeVanishingIdealSingletonForallSet`, `le_zeroLocus_iff_le_vanishingIdeal`, `eq_vanishingIdeal_singleton_of_isMaximal`, `vanishingIdeal_empty`, `zeroLocus_vanishingIdeal_galoisConnection`, `mem_vanishingIdeal_iff`, `mem_vanishingIdeal_singleton_iff`, `instIsMaximalVanishingIdealSingletonForallSet`, `vanishingIdeal_zeroLocus_eq_radical`, `isMaximal_iff_eq_vanishingIdeal_singleton`
`zeroLocus` 📖	CompOp	15 math math: `radical_le_vanishingIdeal_zeroLocus`, `le_vanishingIdeal_zeroLocus`, `zeroLocus_vanishingIdeal_le`, `IsPrime.vanishingIdeal_zeroLocus`, `pointToPoint_zeroLocus_le`, `zeroLocus_bot`, `le_zeroLocus_iff_le_vanishingIdeal`, `mem_zeroLocus_iff`, `zeroLocus_anti_mono`, `zeroLocus_vanishingIdeal_galoisConnection`, `zeroLocus_span`, `zeroLocus_top`, `FirstOrder.Ring.mvPolynomial_zeroLocus_definable`, `ax_grothendieck_zeroLocus`, `vanishingIdeal_zeroLocus_eq_radical`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_vanishingIdeal_singleton_of_isMaximal` 📖	mathematical	—	`vanishingIdeal` `Set` `Set.instSingletonSet`	—	`Algebra.isAlgebraic_iff_isIntegral` `algebraMap_isIntegral_iff` `comp_C_integral_of_surjective_of_isJacobsonRing` `instIsJacobsonRingOfIsArtinianRing` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `instIsDomain` `Ideal.Quotient.isDomain` `Ideal.IsMaximal.isPrime'` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `algHom_ext` `aeval_X` `EuclideanDomain.toNontrivial` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`instIsMaximalVanishingIdealSingletonForallSet` 📖	mathematical	—	`Ideal.IsMaximal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `vanishingIdeal` `Algebra.id` `Set` `Set.instSingletonSet`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Ideal.ext` `RingHom.ker_isMaximal_of_surjective` `algHom_C`
`instIsPrimeVanishingIdealSingletonForallSet` 📖	mathematical	—	`Ideal.IsPrime` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `vanishingIdeal` `Set` `Set.instSingletonSet`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Ideal.ext` `RingHom.ker_isPrime` `instIsDomain`
`isMaximal_iff_eq_vanishingIdeal_singleton` 📖	mathematical	—	`Ideal.IsMaximal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `vanishingIdeal` `Algebra.id` `Set` `Set.instSingletonSet`	—	`eq_vanishingIdeal_singleton_of_isMaximal` `instIsMaximalVanishingIdealSingletonForallSet`
`le_vanishingIdeal_zeroLocus` 📖	mathematical	—	`Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `vanishingIdeal` `zeroLocus`	—	—
`le_zeroLocus_iff_le_vanishingIdeal` 📖	mathematical	—	`Set` `Set.instLE` `zeroLocus` `Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `vanishingIdeal`	—	`GaloisConnection.le_iff_le` `zeroLocus_vanishingIdeal_galoisConnection`
`mem_vanishingIdeal_iff` 📖	mathematical	—	`MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `Ideal` `CommSemiring.toSemiring` `commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `vanishingIdeal` `DFunLike.coe` `AlgHom` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—
`mem_vanishingIdeal_singleton_iff` 📖	mathematical	—	`MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `Ideal` `CommSemiring.toSemiring` `commSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `vanishingIdeal` `Set` `Set.instSingletonSet` `DFunLike.coe` `AlgHom` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—
`mem_zeroLocus_iff` 📖	mathematical	—	`Set` `Set.instMembership` `zeroLocus` `DFunLike.coe` `AlgHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—
`pointToPoint_zeroLocus_le` 📖	mathematical	—	`Set` `PrimeSpectrum` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `commSemiring` `Set.instLE` `Set.image` `pointToPoint` `Algebra.id` `zeroLocus` `PrimeSpectrum.zeroLocus` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`le_trans` `le_vanishingIdeal_zeroLocus` `vanishingIdeal_anti_mono` `Set.singleton_subset_iff`
`radical_le_vanishingIdeal_zeroLocus` 📖	mathematical	—	`Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.radical` `vanishingIdeal` `zeroLocus`	—	`mem_vanishingIdeal_singleton_iff` `Ideal.mem_sInf` `Ideal.radical_eq_sInf` `le_trans` `le_vanishingIdeal_zeroLocus` `vanishingIdeal_anti_mono` `instIsPrimeVanishingIdealSingletonForallSet`
`vanishingIdeal_anti_mono` 📖	mathematical	`Set` `Set.instLE`	`Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `vanishingIdeal`	—	—
`vanishingIdeal_empty` 📖	mathematical	—	`vanishingIdeal` `Set` `Set.instEmptyCollection` `Top.top` `Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`le_antisymm` `le_top` `Set.notMem_empty`
`vanishingIdeal_pointToPoint` 📖	mathematical	—	`PrimeSpectrum.vanishingIdeal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `commSemiring` `Set.image` `PrimeSpectrum` `pointToPoint` `vanishingIdeal`	—	`le_antisymm` `PrimeSpectrum.mem_vanishingIdeal` `instIsPrimeVanishingIdealSingletonForallSet` `Set.mem_singleton_iff`
`vanishingIdeal_zeroLocus_eq_radical` 📖	mathematical	—	`vanishingIdeal` `zeroLocus` `Ideal.radical` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `commSemiring`	—	`le_antisymm` `Ideal.radical_eq_jacobson` `isJacobsonRing` `instIsJacobsonRingOfIsArtinianRing` `isArtinian_of_fg_of_artinian'` `DivisionRing.instIsArtinianRing` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `le_sInf` `eq_vanishingIdeal_singleton_of_isMaximal` `vanishingIdeal_anti_mono` `mem_vanishingIdeal_singleton_iff` `Set.mem_singleton_iff` `radical_le_vanishingIdeal_zeroLocus`
`zeroLocus_anti_mono` 📖	mathematical	`Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Set` `Set.instLE` `zeroLocus`	—	—
`zeroLocus_bot` 📖	mathematical	—	`zeroLocus` `Bot.bot` `Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Top.top` `Set` `BooleanAlgebra.toTop` `Set.instBooleanAlgebra`	—	`eq_top_iff` `Ideal.mem_bot` `RingHom.map_zero`
`zeroLocus_span` 📖	mathematical	—	`zeroLocus` `Ideal.span` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `setOf`	—	`eq_of_forall_le_iff` `le_zeroLocus_iff_le_vanishingIdeal` `Ideal.span_le` `forall₂_swap`
`zeroLocus_top` 📖	mathematical	—	`zeroLocus` `Top.top` `Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Bot.bot` `Set` `BooleanAlgebra.toBot` `Set.instBooleanAlgebra`	—	`eq_bot_iff` `one_ne_zero` `NeZero.one` `EuclideanDomain.toNontrivial` `Submodule.mem_top` `RingHom.map_one`
`zeroLocus_vanishingIdeal_galoisConnection` 📖	mathematical	—	`GaloisConnection` `Ideal` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `commSemiring` `OrderDual` `Set` `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` `vanishingIdeal`	—	`GaloisConnection.monotone_intro` `vanishingIdeal_anti_mono` `zeroLocus_anti_mono` `le_vanishingIdeal_zeroLocus` `zeroLocus_vanishingIdeal_le`
`zeroLocus_vanishingIdeal_le` 📖	mathematical	—	`Set` `Set.instLE` `zeroLocus` `vanishingIdeal`	—	—

MvPolynomial.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`vanishingIdeal_zeroLocus` 📖	mathematical	—	`MvPolynomial.vanishingIdeal` `MvPolynomial.zeroLocus`	—	`MvPolynomial.vanishingIdeal_zeroLocus_eq_radical` `Ideal.IsPrime.radical`

---

← Back to Index