Prime

📁 Source: Mathlib/RingTheory/Ideal/Prime.lean

Statistics

Metric	Count
Definitions IsPrime, primeCompl	2
Theorems mem_of_pow_mem, mem_or_mem, mem_or_mem', mem_or_mem_of_mul_eq_zero, mul_mem_iff_mem_or_mem, mul_mem_left_iff, mul_mem_right_iff, mul_notMem, ne_top, ne_top', one_notMem, pow_mem_iff_mem, bot_prime, eq_bot_of_prime, isPrime_bot, isPrime_iff, mem_primeCompl_iff, notMem_of_isUnit, not_isPrime_iff, one_notMem, of_bot_isPrime	21
Total	23

Ideal

Definitions

Name	Category	Theorems
IsPrime 📖	CompData	114 math math: IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, isPrime_ideal_prod_top, IsArtinianRing.setOf_isPrime_finite, PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible, IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe, PrimeSpectrum.equivSubtype_apply_coe, minimalPrimes_eq_minimals, exists_comap_eq_of_mem_minimalPrimes_of_injective, PrimeSpectrum.equivSubtype_symm_apply_asIdeal, minimalPrimes_isPrime, isPrime_iff_bot_or_prime, sup_primeHeight_eq_ringKrullDim, PrimeSpectrum.denseRange_comap_iff_minimalPrimes, ideal_prod_prime, Localization.localRingHom_injective_of_primesOver_eq_singleton, comap_map_eq_self_iff_of_isPrime, isPrime_map_of_isLocalizationAtPrime, PrimeSpectrum.isPrime, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver, Ring.KrullDimLE.minimalPrimes_eq_setOf_isPrime, isPrime_ideal_prod_top', isPrime_int_iff, exists_ltSeries_length_eq_height, Ring.krullDimLE_zero_and_isLocalRing_tfae, Submodule.IsPrimary.isPrime_radical_colon, Ring.KrullDimLE.existsUnique_isPrime, RingPreordering.instIsPrimeSupport, PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical, exists_ideal_over_prime_of_isIntegral_of_isPrime, MvPolynomial.instIsPrimeVanishingIdealSingletonForallSet, PrimeSpectrum.isIrreducible_zeroLocus_iff, IsPrime.smul_iff, exists_le_prime_disjoint, ProjectiveSpectrum.isPrime, exists_ideal_le_liesOver_of_le, Quotient.isDomain_iff_prime, IsPrime.comap, isPrime_of_maximally_disjoint, isPrime_of_isPrime_prod_top', exists_ideal_comap_le_prime, IsLocalization.isPrime_iff_isPrime_disjoint, PrimeSpectrum.vanishingIdeal_isIrreducible, isPrime_map_quotientMk_of_isPrime, IsLocalization.isPrime_of_isPrime_disjoint, exists_le_prime_notMem_of_isIdempotentElem, IsMaximal.isPrime, isPrime_bot, ValuativeRel.instIsPrimeSupp, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.isPrime_carrier, exists_ideal_over_prime_of_isIntegral_of_isDomain, exists_ideal_lt_liesOver_of_lt, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one', isPrime_of_isPrime_prod_top, radical_eq_sInf, IsHomogeneous.isPrime_iff, IsAssociatedPrime.isPrime, exists_ltSeries_of_hasGoingDown, IsPrime.homogeneousCore, mem_normalizedFactors_iff, isPrime_map_C_of_isPrime, IsHomogeneous.isPrime_of_homogeneous_mem_or_mem, Ring.not_isField_iff_exists_prime, IsPrime.smul, exists_isPrime_liesOver_of_faithfullyFlat, isPrime_of_irreducible_absNorm, ValuationSubring.prime_idealOfLE, not_isPrime_iff, Submodule.isQuotientEquivQuotientPrime_iff, map_isPrime_of_equiv, isPrime_nat_iff, IsLocalization.orderIsoOfPrime_symm_apply_coe, prime_iff_isPrime, Ring.KrullDimLE.mem_minimalPrimes_iff, isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors, primesOver.isPrime, ProjectiveSpectrum.instIsPrimeToIdealNatAsHomogeneousIdeal, RingHom.ker_isPrime, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, isAssociatedPrime_iff_exists_injective_linearMap, IsDiscreteValuationRing.TFAE, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime, comap_isPrime, isPrime_iff_of_isPrincipalIdealRing, IsOka.isPrime_of_maximal_not, Valuation.instIsPrimeSuppOfNontrivialOfNoZeroDivisors, isPrime_radical, map_isPrime_of_surjective, nilradical_eq_sInf, isPrime_iff, mem_minimalPrimes_iff_isPrime, isPrime_of_prime, PrimeSpectrum.isIrreducible_iff_vanishingIdeal_isPrime, exists_comap_eq_of_mem_minimalPrimes, span_singleton_prime, exists_ideal_over_prime_of_isIntegral, PowerSeries.span_X_isPrime, PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite, IsArtinianRing.isPrime_iff_isMaximal, Factors.isPrime, IsPrime.under, IsDedekindDomain.HeightOneSpectrum.isPrime, IsLocalization.orderIsoOfPrime_apply_coe, IsHomogeneous.radical_eq, Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt, isPrime_map_C_iff_isPrime, RingPreordering.IsOrdering.toIsPrime, IsLocalization.AtPrime.isPrime_map_of_liesOver, bot_prime, isMaximal_iff_isPrime, PrimeSpectrum.range_asIdeal, IsMaximal.isPrime', AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.prime, PrimeSpectrum.zeroLocus_eq_singleton
primeCompl 📖	CompOp	219 math math: PrimeSpectrum.mapPiLocalization_id, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_apply, MaximalSpectrum.mapPiLocalization_bijective, PrimeSpectrum.preimageEquivFiber_symm_apply_coe, PrimeSpectrum.residueField_specComap, IsDedekindDomain.HeightOneSpectrum.iInf_localization_eq_bot, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, exists_mem_span_singleton_map_residueField_eq, AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv, ker_algebraMap_residueField, Polynomial.fiberEquivQuotient_tmul, Localization.AtPrime.mapPiEvalRingHom_bijective, Module.rankAtStalk_eq, IsLocalization.AtPrime.mk'_mem_maximal_iff, AlgebraicGeometry.Proj.pow_apply, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.add_mem', instLiesOverFiberOfIsPrime, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, AlgebraicGeometry.Proj.mul_apply, MaximalSpectrum.toPiLocalization_apply_apply, Localization.localRingHom_mk', instIsAlgebraicResidueFieldOfIsIntegral, ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl, instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization, algebraMap_quotient_residueField_mk, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, instIsScalarTowerAtPrimeFractionRing_1, instIsFractionRingAtPrimeFractionRing, Algebra.QuasiFinite.instResidueField, Localization.localRingHom_to_map, AlgebraicGeometry.structureSheafInType.mul_apply, Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Algebra.instFiniteResidueFieldOfQuasiFiniteAt, Localization.localRingHom_injective_of_primesOver_eq_singleton, Algebra.WeaklyQuasiFiniteAt.finite_residueField, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, Localization.AtPrime.isLocalRing, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, AlgebraicGeometry.Proj.one_apply, instIsLocalHomAtPrimeRingHomAlgebraMap, IsLocalizedModule.map_linearMap_of_isLocalization, PrimeSpectrum.coe_preimageHomeomorphFiber_apply_asIdeal, MaximalSpectrum.mapPiLocalization_naturality, AlgebraicGeometry.stalkwise_SpecMap_iff, Localization.AtPrime.eq_maximalIdeal_iff_comap_eq, PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, AlgebraicGeometry.Proj.sub_apply, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, instEssFiniteTypeResidueField_1, Localization.AtPrime.isDedekindDomain, AlgebraicGeometry.StructureSheaf.comap_apply, Fiber.lift_residueField_surjective, AlgebraicGeometry.stalkToFiberRingHom_homogeneousLocalizationToStalk, PrimeSpectrum.mapPiLocalization_bijective, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, algebraMap_residueField_surjective, PrimeSpectrum.toPiLocalization_not_surjective_of_infinite, IsLocalization.instIsScalarTowerLocalizationAtPrime, IsFractionRing.instAtPrimeFractionRing, ResidueField.ringHom_ext_iff, instIsSeparableResidueFieldOfQuotientIdeal, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.mul_mem', disjoint_map_primeCompl_iff_comap_le, PrimeSpectrum.mapPiLocalization_comp, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.neg_mem', surjectiveOnStalks_residueField, PrimeSpectrum.preimageEquivFiber_apply_asIdeal, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom_aux, Algebra.WeaklyQuasiFiniteAt.finite_locoalization, AlgebraicGeometry.ProjectiveSpectrum.Proj.isLocalization_atPrime, PrimeSpectrum.mem_image_comap_basicOpen, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, AlgHom.IsArithFrobAt.localize_algebraMap, AlgebraicGeometry.Spec.germ_stalkMapIso_hom_assoc, PrimeSpectrum.iInf_localization_eq_bot, Localization.localRingHom_id, instIsScalarTowerAtPrimeFractionRing, instIsAlgebraicQuotientIdealResidueField, Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap, Algebra.QuasiFinite.finite_fiber, Algebra.QuasiFinite.instFiniteResidueField, MaximalSpectrum.mapPiLocalization_id, PrimeSpectrum.mapPiLocalization_naturality, Module.rankAtStalk_eq_finrank_tensorProduct, ResidueField.map_algebraMap, algebraMap_mk, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom_assoc, ResidueField.exists_smul_eq_tmul_one, Localization.AtPrime.comap_maximalIdeal, Algebra.isUnramifiedAt_iff_map_eq, Localization.finite_of_primesOver_eq_singleton, Localization.localAlgHom_apply, PrimeSpectrum.toPiLocalization_bijective, PrimeSpectrum.residueField_comap, Algebra.instFiniteResidueFieldOfIsUnramifiedAt, AlgebraicGeometry.StructureSheaf.isLocalizedModule_toPushforwardStalkAlgHom, instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal, AlgebraicGeometry.tilde.instIsLocalizedModuleCarrierCarrierOfCarrierStalkAbPresheafPrimeComplAsIdealHomToStalk, PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective, RingHom.SurjectiveOnStalks.residueFieldMap_bijective, RingHom.surjective_localRingHom_of_surjective, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1, AlgebraicGeometry.Proj.zero_apply, PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.one_mem', Algebra.IsUnramifiedAt.not_minpoly_sq_dvd, Algebra.instIsSeparableResidueFieldOfIsUnramifiedAt, instLiesOverResidueFieldBotIdeal, IsDedekindDomainDvr.is_dvr_at_nonzero_prime, PrimeSpectrum.piLocalizationToMaximal_surjective, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, RingHom.HoldsForLocalization.localRingHom, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv, instFlatAtPrime, mem_primeCompl_iff, AlgebraicGeometry.structureSheafInType.add_apply, Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, IsDedekindDomain.ramificationIdx_eq_one_iff, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv, AlgebraicGeometry.stalkwise_Spec_map_iff, AlgebraicGeometry.Proj.add_apply, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instEssFiniteTypeResidueField, ResidueField.algHom_ext_iff, HomogeneousLocalization.isUnit_iff_isUnit_val, MaximalSpectrum.mapPiLocalization_comp, IsLocalization.instIsScalarTowerAtPrimeFractionRing, isNilpotent_tensor_residueField_iff, Localization.AtPrime.instIsScalarTower_1, Algebra.weaklyQuasiFiniteAt_iff, Localization.AtPrime.instIsScalarTower, PrimeSpectrum.coe_preimageOrderIsoFiber_apply_asIdeal, Module.mem_support_iff_nontrivial_residueField_tensorProduct, instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, AlgHom.IsArithFrobAt.isArithFrobAt_localize, Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes, AlgebraicGeometry.stalkToFiberRingHom_germ, AlgebraicGeometry.StructureSheaf.Localizations.comapFun_mk, Module.notMem_support_iff, instFiniteResidueField, injective_algebraMap_quotient_residueField, HomogeneousLocalization.isLocalRing, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, MaximalSpectrum.iInf_localization_eq_bot, RingHom.Flat.localRingHom, Localization.instFaithfulSMulAtPrimeOfNoZeroDivisors, instIsScalarTowerQuotientIdealResidueField, AlgebraicGeometry.Spec.algebraMap_stalkIso_inv_assoc, Module.mem_support_iff, AlgebraicGeometry.Proj.stalkIso'_germ, disjoint_primeCompl_of_liesOver, MaximalSpectrum.toPiLocalization_injective, AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec, primeCompl_le_nonZeroDivisors, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, RingHom.SurjectiveOnStalks.localRingHom_surjective, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq_comap, AlgebraicGeometry.Scheme.Spec.algebraMap_residueFieldIso_inv_assoc, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection_germ, AlgebraicGeometry.mem_basicOpen_den, IsLocalization.AtPrime.isUnit_mk'_iff, Algebra.instFormallyUnramifiedAtPrimeOfIsUnramifiedAt, MaximalSpectrum.toPiLocalization_not_surjective_of_infinite, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.SectionSubring.zero_mem', Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, Localization.le_comap_primeCompl_iff, IsLocalization.AtPrime.isUnit_to_map_iff, IsLocalization.isLocalization_atPrime_localization_atPrime, Localization.localRingHom_comp, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2, Localization.isLocalHom_localRingHom, PrimeSpectrum.piLocalizationToMaximal_bijective, PrimeSpectrum.toPiLocalization_injective, IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul, Localization.localRingHom_bijective_of_not_conductor_le, AlgebraicGeometry.Spec.germ_stalkMapIso_hom, instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk, Polynomial.residueFieldMapCAlgEquiv_symm_X, Module.mem_freeLocus, Algebra.isSeparable_residueField_iff, algebraMap_residueField_eq_zero, bijective_algebraMap_quotient_residueField, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, Algebra.QuasiFinite.instIsArtinianRingFiber, PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology, RingHom.surjectiveOnStalks_iff_forall_maximal, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1, AlgebraicGeometry.Proj.stalkIso'_symm_mk, AlgebraicGeometry.structureSheafInType.smul_apply, AlgebraicGeometry.localRingHom_comp_stalkIso, Localization.AtPrime.map_eq_maximalIdeal, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, Polynomial.residueFieldMapCAlgEquiv_algebraMap, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, Fiber.exists_smul_eq_one_tmul, AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom, ResidueField.mapₐ_apply, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, PrimeSpectrum.nontrivial_iff_mem_rangeComap, IsLocalization.isDomain_of_local_atPrime, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, Polynomial.residueFieldMapCAlgEquiv_symm_C, PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective, RingHom.surjective_localRingHom_iff, instIsFractionRingQuotientIdealResidueField, AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_prime 📖	mathematical	—	IsPrime Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	isPrime_bot
eq_bot_of_prime 📖	mathematical	—	Bot.bot Ideal DivisionSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	eq_bot_or_top IsPrime.ne_top'
isPrime_bot 📖	mathematical	—	IsPrime Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	one_ne_zero NeZero.one Submodule.mem_bot eq_top_iff_one mul_eq_zero
isPrime_iff 📖	mathematical	—	IsPrime Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsPrime.ne_top' IsPrime.mem_or_mem'
mem_primeCompl_iff 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike primeCompl Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	—
notMem_of_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	IsPrime.ne_top eq_top_of_isUnit_mem
not_isPrime_iff 📖	mathematical	—	IsPrime Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule SetLike.instMembership Submodule.setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
one_notMem 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsPrime.one_notMem

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_of_pow_mem 📖	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	—	one_notMem pow_zero mem_or_mem pow_succ
mem_or_mem 📖	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—	mem_or_mem'
mem_or_mem' 📖	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—	—
mem_or_mem_of_mul_eq_zero 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule	—	mem_or_mem Ideal.zero_mem
mul_mem_iff_mem_or_mem 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mem_or_mem Ideal.mul_mem_right Ideal.mul_mem_left
mul_mem_left_iff 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
mul_mem_right_iff 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mul_mem_iff_mem_or_mem
mul_notMem 📖	mathematical	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	mem_or_mem
ne_top 📖	—	—	—	—	ne_top'
ne_top' 📖	—	—	—	—	—
one_notMem 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Ideal.notMem_of_isUnit isUnit_one
pow_mem_iff_mem 📖	mathematical	—	Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	mem_of_pow_mem Ideal.pow_mem_of_mem

IsDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_bot_isPrime 📖	mathematical	—	IsDomain Ring.toSemiring	—	NoZeroDivisors.to_isDomain Ideal.IsPrime.one_notMem Ideal.IsPrime.mem_or_mem'

---

← Back to Index