Polynomial

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

Statistics

Metric	Count
Definitions	0
Theorems comap_C_surjective, image_comap_C_basicOpen, isOpenMap_comap_C, mem_image_comap_C_basicOpen, comap_C_surjective, exists_image_comap_of_monic, image_comap_C_basicOpen, isCompact_image_comap_of_monic, isOpenMap_comap_C, isOpen_image_comap_of_monic, mem_image_comap_C_basicOpen, exists_image_comap_of_finite_of_free, mem_image_comap_basicOpen, mem_image_comap_zeroLocus_sdiff, isNilpotent_tensor_residueField_iff	15
Total	15

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_C_surjective 📖	mathematical	—	PrimeSpectrum MvPolynomial CommRing.toCommSemiring commSemiring PrimeSpectrum.comap C	—	PrimeSpectrum.comap_comp_apply RingHom.ext eval₂Hom_zero RingHomCompTriple.comp_eq RingHomCompTriple.right_ids constantCoeff_comp_C PrimeSpectrum.comap_id
image_comap_C_basicOpen 📖	mathematical	—	Set.image PrimeSpectrum MvPolynomial CommRing.toCommSemiring commSemiring PrimeSpectrum.comap C SetLike.coe TopologicalSpace.Opens PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen Compl.compl Set Set.instCompl PrimeSpectrum.zeroLocus Set.range Finsupp MulZeroClass.toZero Nat.instMulZeroClass coeff	—	Set.ext mem_image_comap_C_basicOpen
isOpenMap_comap_C 📖	mathematical	—	IsOpenMap PrimeSpectrum MvPolynomial CommRing.toCommSemiring commSemiring PrimeSpectrum.zariskiTopology PrimeSpectrum.comap C	—	TopologicalSpace.IsTopologicalBasis.open_eq_sUnion PrimeSpectrum.isTopologicalBasis_basic_opens Set.image_sUnion isOpen_sUnion image_comap_C_basicOpen IsClosed.isOpen_compl PrimeSpectrum.isClosed_zeroLocus
mem_image_comap_C_basicOpen 📖	mathematical	—	PrimeSpectrum CommRing.toCommSemiring Set Set.instMembership Set.image MvPolynomial commSemiring PrimeSpectrum.comap C SetLike.coe TopologicalSpace.Opens PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal coeff	—	PrimeSpectrum.isPrime Algebra.to_smulCommClass PrimeSpectrum.mem_image_comap_basicOpen not_iff_not IsNilpotent.map_iff RingHomClass.toMonoidWithZeroHomClass IsScalarTower.right AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.injective isNilpotent_iff_eq_zero isReduced_of_noZeroDivisors instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain ringHom_ext' RingHom.ext ext smulCommClass RingHomCompTriple.comp_apply RingHomCompTriple.right_ids rTensorAlgEquiv_apply coeff_map coeff_rTensorAlgHom_tmul coeff_C Algebra.smul_def map_zero MonoidWithZeroHomClass.toZeroHomClass RingHom.instRingHomClass mul_one map_C coeff_X' ite_smul one_smul zero_smul map_X

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_C_surjective 📖	mathematical	—	PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring PrimeSpectrum.comap C	—	PrimeSpectrum.comap_comp_apply RingHom.ext eval_C PrimeSpectrum.comap_id
exists_image_comap_of_monic 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring	Set.image PrimeSpectrum Polynomial commSemiring PrimeSpectrum.comap C Set Set.instSDiff PrimeSpectrum.zeroLocus Set.instSingletonSet Compl.compl Set.instCompl SetLike.coe Finset Finset.instSetLike	—	PrimeSpectrum.exists_image_comap_of_finite_of_free Module.Finite.of_basis IsScalarTower.right Finite.of_fintype Module.Free.of_basis
image_comap_C_basicOpen 📖	mathematical	—	Set.image PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring PrimeSpectrum.comap C SetLike.coe TopologicalSpace.Opens PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen Compl.compl Set Set.instCompl PrimeSpectrum.zeroLocus Set.range coeff	—	Set.ext mem_image_comap_C_basicOpen
isCompact_image_comap_of_monic 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring	IsCompact PrimeSpectrum PrimeSpectrum.zariskiTopology Set.image Polynomial commSemiring PrimeSpectrum.comap C Set Set.instSDiff PrimeSpectrum.zeroLocus Set.instSingletonSet	—	exists_image_comap_of_monic Set.iUnion_of_singleton_coe PrimeSpectrum.zeroLocus_iUnion Set.compl_iInter isCompact_iUnion Finite.of_fintype PrimeSpectrum.basicOpen_eq_zeroLocus_compl PrimeSpectrum.isCompact_basicOpen
isOpenMap_comap_C 📖	mathematical	—	IsOpenMap PrimeSpectrum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring PrimeSpectrum.zariskiTopology PrimeSpectrum.comap C	—	TopologicalSpace.IsTopologicalBasis.open_eq_sUnion PrimeSpectrum.isTopologicalBasis_basic_opens Set.image_sUnion isOpen_sUnion image_comap_C_basicOpen IsClosed.isOpen_compl PrimeSpectrum.isClosed_zeroLocus
isOpen_image_comap_of_monic 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring	IsOpen PrimeSpectrum PrimeSpectrum.zariskiTopology Set.image Polynomial commSemiring PrimeSpectrum.comap C Set Set.instSDiff PrimeSpectrum.zeroLocus Set.instSingletonSet	—	exists_image_comap_of_monic IsClosed.isOpen_compl PrimeSpectrum.isClosed_zeroLocus
mem_image_comap_C_basicOpen 📖	mathematical	—	PrimeSpectrum CommRing.toCommSemiring Set Set.instMembership Set.image Polynomial CommSemiring.toSemiring commSemiring PrimeSpectrum.comap C SetLike.coe TopologicalSpace.Opens PrimeSpectrum.zariskiTopology TopologicalSpace.Opens.instSetLike PrimeSpectrum.basicOpen Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal coeff	—	PrimeSpectrum.isPrime Algebra.to_smulCommClass PrimeSpectrum.mem_image_comap_basicOpen not_iff_not IsNilpotent.map_iff RingHomClass.toMonoidWithZeroHomClass IsScalarTower.right AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.injective isNilpotent_iff_eq_zero isReduced_of_noZeroDivisors instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain ringHom_ext' RingHom.ext ext RingHomCompTriple.comp_apply RingHomCompTriple.right_ids map_C one_smul map_X coeff_map

PrimeSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_image_comap_of_finite_of_free 📖	mathematical	—	Set.image PrimeSpectrum CommRing.toCommSemiring comap algebraMap CommSemiring.toSemiring Set Set.instSDiff zeroLocus Set.instSingletonSet Compl.compl Set.instCompl SetLike.coe Finset Finset.instSetLike	—	IsScalarTower.right smulCommClass_self IsScalarTower.left Ideal.instIsTwoSided_1 Set.ext isPrime Submodule.Quotient.smulCommClass Algebra.to_smulCommClass mem_image_comap_zeroLocus_sdiff IsScalarTower.algebraMap_apply TensorProduct.isScalarTower_left isNilpotent_tensor_residueField_iff Finset.coe_image Finset.coe_range
mem_image_comap_basicOpen 📖	mathematical	—	PrimeSpectrum CommRing.toCommSemiring Set Set.instMembership Set.image comap algebraMap CommSemiring.toSemiring SetLike.coe TopologicalSpace.Opens zariskiTopology TopologicalSpace.Opens.instSetLike basicOpen IsNilpotent TensorProduct Ideal.ResidueField asIdeal isPrime NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id TensorProduct.zero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.instSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass	—	isPrime IsScalarTower.right Algebra.to_smulCommClass Submodule.Quotient.smulCommClass Ideal.Quotient.isScalarTower Ideal.span_empty Ideal.instIsTwoSidedBot RingEquiv.map_mul' RingEquiv.map_add' AlgHom.commutes' IsNilpotent.map_iff RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.injective AlgEquiv.commutes mem_image_comap_zeroLocus_sdiff zeroLocus_empty Set.compl_eq_univ_diff basicOpen_eq_zeroLocus_compl
mem_image_comap_zeroLocus_sdiff 📖	mathematical	—	PrimeSpectrum CommRing.toCommSemiring Set Set.instMembership Set.image comap algebraMap CommSemiring.toSemiring Set.instSDiff zeroLocus Set.instSingletonSet IsNilpotent TensorProduct HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.span Ideal.ResidueField asIdeal isPrime NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Submodule.Quotient.module' CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul Algebra.toModule IsScalarTower.right DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id TensorProduct.zero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.instSemiring Ideal.Quotient.semiring Ideal.instAlgebraQuotient DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Algebra.TensorProduct.leftAlgebra Submodule.Quotient.smulCommClass Ring.toSemiring Algebra.to_smulCommClass	—	isPrime IsScalarTower.right Submodule.Quotient.smulCommClass Algebra.to_smulCommClass RingHom.instRingHomClass Ideal.span_le Ideal.ker_algebraMap_residueField Ideal.IsPrime.under Ideal.Quotient.isScalarTower IsLocalRing.instIsScalarTowerResidueField OreLocalization.instIsScalarTower Ideal.instIsTwoSided_1 Commute.all IsNilpotent.map RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.mem_ker isNilpotent_iff_eq_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain AlgHom.commutes Ideal.mem_sInf nilradical_eq_sInf mem_nilradical Ideal.Quotient.eq_zero_iff_mem Ideal.subset_span TensorProduct.zero_tmul AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass comap_comp_apply IsScalarTower.algebraMap_eq TensorProduct.isScalarTower_left AlgHom.comp_algebraMap Unique.instSubsingleton ext Ideal.ext

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_tensor_residueField_iff 📖	mathematical	—	IsNilpotent TensorProduct CommRing.toCommSemiring Ideal.ResidueField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsLocalRing.instCommRingResidueField Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl CommSemiring.toSemiring OreLocalization.oreSetComm CommSemiring.toCommMonoid Algebra.toModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id TensorProduct.zero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Algebra.TensorProduct.instSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass Ideal SetLike.instMembership Submodule.setLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Polynomial.coeff LinearMap.charpoly Ring.toAddCommGroup CommRing.toRing AlgHom Module.End Module.End.instSemiring Module.End.instAlgebra smulCommClass_self DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left AlgHom.funLike Algebra.lmul	—	subsingleton_or_nontrivial Algebra.to_smulCommClass smulCommClass_self IsScalarTower.left RingHom.codomain_trivial IsScalarTower.right Module.finrank_subsingleton Unique.instSubsingleton IsScalarTower.to_smulCommClass Module.finrank_tensorProduct commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.self Module.finrank_self one_mul IsNilpotent.map_iff RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.injective AlgHom.algHomClass Algebra.lmul_injective Module.Free.tensor Module.Finite.base_change LinearMap.isNilpotent_iff_charpoly instIsDomain Algebra.baseChange_lmul LinearMap.charpoly_baseChange LinearMap.charpoly_natDegree RingHom.instRingHomClass Polynomial.coeff_map Polynomial.coeff_X_pow LT.lt.ne Ideal.ker_algebraMap_residueField Polynomial.ext eq_or_ne Polynomial.leadingCoeff.eq_1 LinearMap.charpoly_monic map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass lt_or_gt_of_ne Polynomial.coeff_eq_zero_of_natDegree_lt map_zero MonoidWithZeroHomClass.toZeroHomClass LT.lt.ne'

---

← Back to Index