Ideal

📁 Source: Mathlib/Topology/Algebra/Ring/Ideal.lean

Statistics

Metric	Count
Definitions Ideal, closure, connectedComponentOfZero, topologicalRingQuotientTopology	4
Theorems closure_eq_of_isClosed, coe_closure, coe_connectedComponentOfZero, isOpenMap_coe, isOpenQuotientMap_mk, isQuotientMap_coe_coe, instCompactSpaceQuotientIdeal, topologicalRing_quotient	8
Total	12

Ideal

Definitions

Name	Category	Theorems
closure 📖	CompOp	6 math math: closure_eq_of_isClosed, coe_closure, ContinuousMap.idealOfSet_ofIdeal_eq_closure, UniformSpace.inseparableSetoid_ring, IsMaximal.closure_eq, ContinuousMap.idealOpensGI_choice
connectedComponentOfZero 📖	CompOp	1 math math: coe_connectedComponentOfZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_eq_of_isClosed 📖	mathematical	—	closure	—	SetLike.ext' IsClosed.closure_eq
coe_closure 📖	mathematical	—	SetLike.coe Ideal Ring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule closure closure	—	—
coe_connectedComponentOfZero 📖	mathematical	—	SetLike.coe Ideal Ring.toSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule connectedComponentOfZero connectedComponent MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—

QuotientRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenMap_coe 📖	mathematical	—	IsOpenMap HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient topologicalRingQuotientTopology DFunLike.coe RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	QuotientAddGroup.isOpenMap_coe instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing
isOpenQuotientMap_mk 📖	mathematical	—	IsOpenQuotientMap HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient topologicalRingQuotientTopology DFunLike.coe RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing
isQuotientMap_coe_coe 📖	mathematical	—	Topology.IsQuotientMap HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient instTopologicalSpaceProd topologicalRingQuotientTopology DFunLike.coe RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 RingHom.instFunLike	—	IsOpenQuotientMap.isQuotientMap Ideal.instIsTwoSided_1 IsOpenQuotientMap.prodMap

(root)

Definitions

Name	Category	Theorems
Ideal 📖	CompOp	2675 math math: Ideal.mem_bot, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, Ideal.exists_pow_le_of_le_radical_of_fg_radical, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Polynomial.coeff_prod_mem_ideal_pow_tsub, Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ, MvPolynomial.vanishingIdeal_anti_mono, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', Ideal.isPrime_ideal_prod_top, Ideal.toCotangent_to_quotient_square, Ideal.Quotient.nontrivial_of_liesOver_of_isPrime, FractionalIdeal.coeIdeal_top, Submodule.instIsScalarTowerQuotientIdealSubtypeMemTorsionBySetCoe, Polynomial.not_ker_le_map_C_of_surjective_of_quasiFiniteAt, KaehlerDifferential.kerCotangentToTensor_toCotangent, Ideal.Quotient.isScalarTower, PrimeSpectrum.closure_range_comap, Ideal.radical_mono, Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, Ideal.Quotient.exists_algHom_fixedPoint_quotient_under, Ideal.maximal_of_no_maximal, IsDedekindDomain.differentIdeal_dvd_map_differentIdeal, IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span, Submodule.colon_empty, Ideal.mem_image_of_mem_map_of_surjective, Submodule.mem_colon_span_singleton, IsLocalization.surjective_quotientMap_of_maximal_of_localization, DividedPowers.dpow_mem, IsArtinianRing.setOf_isPrime_finite, AdicCompletion.val_sub_apply, Ideal.radical_sup, Algebra.exists_unramified_of_isUnramifiedAt, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, Ideal.comap_fiberIsoOfBijectiveResidueField_apply, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, Ideal.span_le, Ideal.comap_bot_le_of_injective, Irreducible.maximalIdeal_eq_setOf_le_v_coe, Algebra.FiniteType.quotient, Ideal.selfBasis_def, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, AlgebraicGeometry.Scheme.zeroLocus_iInf, PrimeSpectrum.vanishingIdeal_isClosed_isIrreducible, Submodule.supIndep_torsionBySet_ideal, Ideal.dvd_iff_le, DoubleQuot.liftSupQuotQuotMkₐ_toRingHom, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, MvPolynomial.radical_le_vanishingIdeal_zeroLocus, derivationToSquareZeroOfLift_apply, Ideal.eq_jacobson_iff_sInf_maximal, IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply, Ideal.subset_union, ValuationSubring.valuation_lt_one_iff, Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, Module.mem_annihilator, Ideal.Cotangent.lift_comp_toCotangent, Ideal.tensorCotangentEquiv_tmul, Ideal.pow_multiset_sum_mem_span_pow, Module.support_quotient, Ideal.Quotient.map_ker_stabilizer_subtype, HomogeneousIdeal.toIdeal_mul, PadicInt.lift_sub_val_mem_span, Valuation.ltIdeal_le_leIdeal, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, Ideal.finite_setOf_absNorm_le₀, Valuation.supp_quot_supp, Polynomial.mem_image_comap_C_basicOpen, IsAdicComplete.StrictMono.mk_liftRingHom, Ideal.hasFiniteMulSupport_coe, ClassGroup.mk0_integralRep, Ideal.mul_eq_inf_of_coprime, ValuationSubring.image_maximalIdeal, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, cardQuot_mul, Int.quotientSpanEquivZMod_comp_Quotient_mk, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, Ideal.IsTwoSided.pow_succ, Submodule.le_annihilator_iff, Polynomial.Monic.free_quotient, StandardEtalePair.inv_aeval_X_g, PrimeSpectrum.asIdeal_bot, Ideal.eq_bot_of_comap_eq_bot', Ideal.span_singleton_mul_le_span_singleton_mul, Ideal.mem_span_iff_exists_isHomogeneous, Ideal.exists_smith_normal_form, Submodule.mem_ideal_smul_span_iff_exists_sum, IdealFilter.IsUniform.colon_mem, ClassGroup.mk0_eq_mk0_iff, Algebra.Presentation.naive_toGenerators, Valuation.mem_maximalIdeal_iff, Algebra.TensorProduct.quotIdealMapEquivQuotTensor_mk, IsLocalization.coeSubmodule_mul, PrimeSpectrum.localization_specComap_range, Ideal.toCotangent_eq, Ideal.subset_span, AdicCompletion.AdicCauchySequence.mk_eq_mk, IsLocalization.minimalPrimes_map, Ideal.absNorm_span_insert, Ideal.le_comap_of_map_le, Ideal.comap_inf, Ideal.map_eq_top_iff_of_ker_le, Valuation.mem_supp_iff, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_apply_mk, IdealFilter.ringFilterBasis_sets, RingTheory.Sequence.isWeaklyRegular_cons_iff', NumberField.isCoprime_differentIdeal_of_isCoprime_discr, Ideal.single_mem_pi, Submodule.smul_eq_map₂, Ideal.squarefree_span_singleton, Ideal.mem_span_singleton', Ideal.mem_ofPolynomial, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, Ideal.height_le_iff_exists_minimalPrimes, Ideal.under_bot, IsAdjoinRoot.mem_ker_map, Module.associatedPrimes.mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule, Submodule.isInternal_prime_power_torsion_of_pid, SModEq.pow_pow_add_one, Ideal.relNorm_smul, AssociatedPrimes.mem_iff, IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe, ClassGroup.mk_eq_mk_of_coe_ideal, differentIdeal_eq_differentIdeal_mul_differentIdeal, IsFractionRing.coeSubmodule_strictMono, smoothSheafCommRing.nonunits_stalk, FractionalIdeal.coeIdealHom_apply, AdicCompletion.map_val_apply, Ideal.mul_le_right, mem_reesAlgebra_iff_support, Ideal.isHomogeneous_iff_subset_iInter, Ideal.quotientEquiv_symm_apply, Perfection.mk_comp_teichmuller₀, PrimeSpectrum.zeroLocus_nilradical, RingEquiv.idealComapOrderIso_apply, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, Ideal.exists_mem_span_singleton_map_residueField_eq, AlgebraicGeometry.LocallyRingedSpace.notMem_prime_iff_unit_in_stalk, algebraicIndependent_iff_ker_eq_bot, RingHom.ker_eq_top_of_subsingleton, Ideal.smul_top_eq_map, MvPowerSeries.mem_hasEvalIdeal_iff, IsLocalRing.map_maximalIdeal_le, Ideal.rank_prime_pow_ramificationIdx, Ideal.algebraMap_quotient_injective, Submodule.coe_mapAlgEquiv_symm_apply, Matrix.coeff_charpoly_mem_ideal_pow, PrimeSpectrum.zeroLocus_eq_univ_iff, Ideal.exists_nonzero_mem_of_ne_bot, RingHom.eq_liftOfRightInverse, Submodule.mul_annihilator, finrank_quotient_span_eq_natDegree_norm, WithIdealFilter.mem_nhds_zero_iff, normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, span_singleton_dvd_span_singleton_iff_dvd, Ideal.le_span_singleton_mul_iff, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', Ring.coe_jacobson_quotient, Ideal.mem_leadingCoeffNth_zero, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, Ideal.coe_smul_primesOver_mk_eq_map_galRestrict, IdealFilter.isPFilter_gabrielComposition, PrimeSpectrum.equivSubtype_apply_coe, DividedPowers.IsDPMorphism.ideal_comp, Ideal.exists_maximal, Polynomial.fiberEquivQuotient_tmul, ProjectiveSpectrum.zeroLocus_mul_ideal, Ideal.coeff_zero_mem_comap_of_root_mem_of_eval_mem, Submodule.mem_colon', Ideal.map_pi, PadicInt.appr_spec, minimalPrimes_eq_minimals, Ring.isField_iff_isSimpleOrder_ideal, Ideal.sum_eq_sup, Ideal.one_eq_top, IsLocalization.AtPrime.mk'_mem_maximal_iff, idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical, Ideal.quotientMap_comp_mk, IsArithFrobAt.exists_primesOver_isConj, Ideal.mem_colon_span_singleton, Ideal.IsHomogeneous.sInf, range_comap_of_surjective, Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, Ideal.under_top, PrimeSpectrum.isRetrocompact_zeroLocus_compl_of_fg, Ideal.height_top, Ideal.natCast_eq_top, Ideal.intNorm_mem_spanNorm, Ideal.smul_closure, ringKrullDim_eq_one_iff_of_isLocalRing_isDomain, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, RingHom.quotientKerEquivOfSurjective_symm_apply, Polynomial.contentIdeal_one, Ideal.Quotient.factor_comp_mk, Ideal.exists_comap_eq_of_mem_minimalPrimes_of_injective, IsDedekindDomain.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime, Ideal.instCanLiftTwoSidedIdealCoeOrderHomAsIdealIsTwoSided, Ideal.prime_of_mem_primesOver, Ideal.mem_sSup_of_mem, IsLocalizedModule.exists_subsingleton_away, Associates.finite_factors, MvPolynomial.le_vanishingIdeal_zeroLocus, Ideal.comap_cotangentIdeal, RingPreordering.coe_support, Polynomial.quotientSpanXSubCAlgEquiv_symm_apply, PrimeSpectrum.equivSubtype_symm_apply_asIdeal, Module.isTorsionBySet_quotient_ideal_smul, IsLocalization.map_eq_top_of_not_subset, QuotSMulTop.equivTensorQuot_naturality, DoubleQuot.coe_quotQuotMkₐ, Ideal.isHomogeneous_iff_forall_subset, Ideal.Quotient.factorₐ_comp_mk, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal', Valuation.mem_ltIdeal_iff, PrimeSpectrum.discreteTopology_iff_finite_isMaximal_and_sInf_le_nilradical, KaehlerDifferential.cotangentComplexBaseChange_tmul, NumberField.FinitePlace.norm_def', DividedPowers.OfInvertibleFactorial.dpow_apply, Ideal.mem_pointwise_smul_iff_inv_smul_mem, Ideal.span_pow_eq_map_homogeneousSubmodule, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_mk, IsArtinianRing.primeSpectrum_asIdeal_range_eq, Ideal.span_singleton_mul_left_injective, PadicInt.sub_zmodRepr_mem, Int.quotientSpanNatEquivZMod_comp_Quotient_mk, Submodule.ideal_span_singleton_smul, Ideal.finite_setOf_absNorm_eq, IsLocalRing.finrank_quotient_map, DividedPowers.SubDPIdeal.sInf_carrier_def, StandardEtalePresentation.toPresentation_algebra_smul, Module.supportDim_eq_ringKrullDim_quotient_annihilator, Submodule.top_eq_ofList_cons_smul_iff, Ideal.exists_smul_eq_of_isGaloisGroup, ContinuousMap.notMem_idealOfSet, Ring.DimensionLEOne.eq_bot_of_lt, Ideal.quotient_map_C_eq_zero, PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical, ValuationRing.le_total_ideal, RingHom.liftOfSurjective_comp, AlgebraicGeometry.Scheme.zeroLocus_mul, Ideal.exists_finset_card_eq_height_of_isNoetherianRing, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, PrimeSpectrum.gc, exists_spanRank_le_and_le_height_of_le_height, AdicCompletion.val_smul, DividedPowers.isSubDPIdeal_iInf, PrimeSpectrum.vanishingIdeal_strict_anti_mono_iff, Valuation.Integers.isPrincipal_iff_exists_isGreatest, Submodule.sup_eq_sup_smul_of_le_smul_of_le_jacobson, Polynomial.IsDistinguishedAt.map_eq_X_pow, TruncatedWittVector.iInf_ker_truncate, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, Ideal.subset_pointwise_smul_iff, Ideal.IsPrime.prod_le, isUnit_iff_notMem_of_isAdicComplete_maximal, AlgebraicIndependent.repr_ker, Module.FinitePresentation.exists_notMem_bijective, Submodule.mem_smul_span_singleton, AlgHom.IsArithFrobAt.mk_apply, Localization.localRingHom_mk', Ideal.map_mk_comap_factor, WittVector.factorPowSucc_comp_fontaineThetaModPPow, PowerBasis.quotientEquivQuotientMinpolyMap_apply, DoubleQuot.coe_quotLeftToQuotSupₐ, Ideal.bot_lt_of_maximal, range_specComap_of_surjective, AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp, AdicCompletion.incl_apply, Module.mem_support_iff_of_finite, Ideal.quotientInfToPiQuotient_inj, HomogeneousIdeal.toIdeal_add, DividedPowers.SubDPIdeal.le_iff, Algebra.IsSmoothAt.exists_notMem_isStandardSmooth, Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, AdicCompletion.val_smul_eq_evalₐ_smul, nilradical_le_prime, FractionalIdeal.count_well_defined, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_apply, Ideal.inertiaDeg_algebraMap, PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal, ValuationRing.TFAE, Ideal.torsionMapQuot_apply, Ideal.notMem_of_isUnit, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Ideal.isPrime_iff_bot_or_prime, DividedPowers.OfInvertibleFactorial.dpow_mem, Ideal.span_singleton_eq_bot, Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, NumberField.HeightOneSpectrum.rankOne_hom'_def, Ideal.Quotient.algEquivOfEqMap_apply, Ideal.range_cotangentToQuotientSquare, Ideal.Filtration.smul_le, Ideal.Quotient.factor_mk, AdicCompletion.exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top, IsLocalization.mem_span_map, Ideal.mem_toTwoSided, Module.supportDim_add_length_eq_supportDim_of_isRegular, Algebra.QuasiFinite.instQuotientIdeal, TwoSidedIdeal.instIsTwoSidedCoeOrderHomIdealAsIdeal, Ideal.ne_top_iff_one, Ideal.coe_connectedComponentOfZero, Ideal.Factors.fact_ramificationIdx_neZero, Ideal.IsPrime.mem_pow_mul, Ideal.algebraMap_quotient_residueField_mk, instIsSeparableQuotientIdealOfResidueField, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, HomogeneousIdeal.toIdeal_iInf, Ideal.span_pow_eq_top, instFiniteQuotientRingOfIntegersIdealOfNumberFieldOfIsMaximal, IsDedekindDomain.HeightOneSpectrum.isCoprime_of_ne, Ideal.relNorm_mono, Ideal.sup_primeHeight_eq_ringKrullDim, exists_le_isAssociatedPrime_of_isNoetherianRing, FractionalIdeal.absNorm_eq', finrank_quotient_span_eq_natDegree', prod_normalizedFactors_eq_self, Ideal.Quotient.instFaithfulSMul, Ideal.quotientInfToPiQuotient_surj, IsSemisimpleModule.jacobson_le_annihilator, IsAdicComplete.mkQ_comp_lift, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal, Ideal.exists_eq_mul_of_pure, Ideal.map_spanIntNorm, Ideal.LiesOver.smul, Ideal.IsPrime.pow_mem_iff_mem, QuotientMapQuotient.isNoetherian, Ideal.minimalPrimes_top, KaehlerDifferential.kerToTensor_apply, AlgEquiv.prodQuotientOfIsIdempotentElem_apply, Ideal.ncard_primesOver_mul_ncard_primesOver, HenselianLocalRing.is_henselian, RingHom.ker_equiv, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule, Algebra.Presentation.differentials.hom₁_single, RingOfIntegers.exponent_eq_sInf, RingHom.SurjectiveOnStalks.exists_mul_eq_tmul, Ideal.iInf_mul, Ideal.relNorm_relNorm, Algebra.zariskisMainProperty_iff, PrimeSpectrum.denseRange_comap_iff_minimalPrimes, Algebra.Generators.exists_presentation_of_basis_cotangent, DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv, Ideal.mul_sup_eq_of_coprime_right, Ideal.map_under_le_under_map, Ideal.mem_toCotangent_ker, RingHom.liftOfSurjective_comp_apply, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, Ideal.ideal_prod_prime, Ideal.absNorm_pos_iff_mem_nonZeroDivisors, Ideal.spanNorm_mono, Module.associatedPrimes.mem_associatePrimes_localizedModule_atPrime_of_mem_associated_primes, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Ideal.comap_finsetInf, Submodule.colon_finsetInf, Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown, IsLocalization.coe_primeSpectrumOrderIso_symm_apply_asIdeal, Ideal.Quotient.tower_quotient_map_quotient, nilradical_eq_zero, Nat.exists_mem_span_nat_finset_of_ge, Ideal.map_eq_top_or_isMaximal_of_surjective, DoubleQuot.quotQuotEquivComm_symmₐ, ringKrullDim_quotient, Ideal.liesOver_iff_dvd_map, Ideal.Quotient.subsingleton_iff, Localization.localRingHom_injective_of_primesOver_eq_singleton, Ideal.finsuppTotal_apply_eq_of_fintype, WittVector.factorPowSucc_fontaineThetaModPPow_eq, Ideal.Quotient.coe_factorₐ, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical, Ideal.Quotient.factor_comp_apply, QuotSMulTop.equivTensorQuot_naturality_mk, IsSimpleRing.tfae, DividedPowers.SubDPIdeal.dpow_mem_span_of_mem_span, IsLocalRing.map_mkQ_eq, Ideal.comap_map_eq_self_iff_of_isPrime, Ideal.jacobson_bot, Ideal.bot_pow, Ideal.mem_iff_of_associated, Submodule.mem_ideal_smul_span_iff_exists_sum', Ideal.FG.pow, TwoSidedIdeal.bot_asIdeal, PrimeSpectrum.vanishingIdeal_irreducibleComponents, IdealFilter.isTorsionQuot_inter_left_iff, MvPolynomial.pow_idealOfVars, IsLocalRing.maximalIdeal_le_jacobson, Algebra.EssFiniteType.quotient_map, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal, Ideal.pow_sup_eq_top, Ring.jacobson_smul_top_le, Ideal.absNorm_eq_pow_inertiaDeg', IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, biUnion_associatedPrimes_eq_compl_regular, ContinuousMap.mem_idealOfSet, Algebra.Extension.lTensor_cotangentComplex_eq_cotangentComplexBaseChange, DirectSum.decompose_eq_mul_idempotent, irreducible_pow_sup_of_ge, Ideal.exists_pow_le_of_le_radical_of_fg, ClassGroup.mk0_eq_one_iff, idealFactorsFunOfQuotHom_comp, Ring.DimensionLEOne.not_lt_lt, Ideal.quotientEquivAlg_mk, IsLocalRing.maximal_ideal_unique, Submodule.comap_smul_top_of_surjective, pow_sub_one_dvd_differentIdeal, Submodule.pow_smul_top_le, Module.associatedPrimes.preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule, IsLocalRing.residue_eq_zero_iff, Ring.jacobson_quotient_of_le, Polynomial.mem_iff_eq_smul_annIdealGenerator, Ideal.exists_maximal_ideal_liesOver_of_isIntegral, PrimeSpectrum.vanishingIdeal_anti_mono_iff, MvPolynomial.mem_pow_idealOfVars_iff, Ideal.mem_minimalPrimes_of_height_eq, Ideal.finsuppTotal_apply, Ideal.pow_sup_pow_eq_top, IsLocalization.AtPrime.coe_orderIsoOfPrime_symm_apply_coe, Ideal.exists_mul_mem_of_mem_minimalPrimes, coe_primesOverFinset, TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor, Ideal.subset_union_prime', Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, Ideal.prod_mem, Ideal.quotientEquivAlgOfEq_coe_eq_factor, RingHom.quotientKerEquivOfSurjective_symm_comp, Ideal.mem_map_of_mem, Ideal.count_normalizedFactors_eq, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf, Ideal.rootsOfUnityMapQuot_injective, Ideal.sInf_isPrime_of_isChain, Ideal.relNorm_top, Ideal.Quotient.factorₐ_apply_mk, AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, Valuation.ltIdeal_v_le_of_mem, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, DividedPowers.mem_dpEqualizer_iff, PrimeSpectrum.union_zeroLocus, Ideal.Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, HomogeneousIdeal.eq_bot_iff, AlgebraicGeometry.Scheme.zeroLocus_biInf, Ideal.le_of_localization_maximal, Ideal.gcd_eq_sup, IsPrecomplete.bot, Ideal.toTwoSided_asIdeal, Ideal.mul_eq_inf_of_isCoprime, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpec, Ring.KrullDimLE.minimalPrimes_eq_setOf_isPrime, algebra_finiteType_of_liesOver, Ideal.relNorm_eq_pow_of_isPrime_isGalois, instIsPrimeValIdealMemSetAssociatedPrimes, IsLocalRing.basisQuotient_repr, Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver, Ideal.comap_iInf, Ideal.Quotient.algebraMap_quotient_of_ramificationIdx_neZero, Ideal.mul_comm, Ideal.absNorm_mem, Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRing, Ideal.map_mul, Ideal.prime_span_singleton_iff, Submodule.map_smul'', Ideal.prod_bot_bot, Ideal.isIdempotentElem_iff_eq_bot_or_top, Ideal.mul_bot, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, Ideal.sup_eq_top_iff_isCoprime, Ideal.le_radical, AlgEquiv.quotientBot_mk, AdicCompletion.pi_apply_coe, PreValuationRing.iff_ideal_total, Ideal.smul_sup, Ideal.comap_le_map_of_inverse, Algebra.Extension.Cotangent.val_mk, Ideal.smul_eq_mul, Ideal.Quotient.stabilizerHom_surjective, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, RingEquiv.quotientBot_symm_mk, Ideal.isPrime_ideal_prod_top', RingTheory.Sequence.isWeaklyRegular_iff_Fin, Ideal.isPrimary_finsetInf, Ideal.quotEquivOfEq_mk, Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn, AlgebraicGeometry.stalkwise_SpecMap_iff, Ideal.factors_decreasing, span_le_of_C_coeff_mem, PrimeSpectrum.iSup_basicOpen_eq_top_iff, AdicCompletion.val_add_apply, Ideal.Quotient.algebraMap_eq, Ideal.prod_mono_left, Submodule.annihilator_iSup, Ideal.injective_quotient_le_comap_map, DividedPowers.SubDPIdeal.isSubideal, IsLocalRing.exists_maximalIdeal_pow_le_of_finite_quotient, AdicCompletion.ofPowSMul_ofValEqZero, Ideal.Quotient.algebraMap_quotient_map_quotient, Perfection.mk_teichmuller, Submodule.iInf_colon_iSup, AdicCompletion.smul_eval, Ideal.pointwise_smul_subset_iff, TensorProduct.quotTensorEquivQuotSMul_mk_one_tmul, Ideal.isPrime_int_iff, IsLocalRing.mem_maximalIdeal, retractionOfSectionOfKerSqZero_comp_kerToTensor, PadicInt.exists_mem_range, is_bot_adic_iff, PreTilt.mk_comp_untilt_eq_coeff_zero, DoubleQuot.quotQuotEquivComm_comp_quotQuotMk, Ideal.ramificationIdx_ne_one_iff, Ideal.toCotangent_range, Ideal.mem_sup_left, HenselianRing.is_henselian, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', Algebra.Presentation.quotientEquiv_symm, FractionalIdeal.mem_coeSubmodule, PrimeSpectrum.zeroLocus_subset_zeroLocus_iff, DoubleQuot.quotQuotEquivComm_quotQuotMk, Module.Invertible.exists_linearEquiv_ideal, Ideal.instCovariantClassHSMulLe, Submodule.colon_union, Ideal.prod_le_inf, Polynomial.Monic.quotient_isIntegral, Ideal.Quotient.exists_inv, IsLocalization.AtPrime.coe_primeSpectrumOrderIso_apply_coe_asIdeal, Ring.krullDimLE_zero_and_isLocalRing_tfae, WittVector.mk_pow_fontaineTheta, Localization.exists_finite_awayMapₐ_of_surjective_awayMapₐ, Ideal.ker_Pi_Quotient_mk, Ideal.adic_module_basis, Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective, Ideal.minimalPrimes_eq_subsingleton, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange_residueField, Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd, PrimeSpectrum.coe_preimageOrderIsoFiber_symm_apply_coe_asIdeal, AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHom, Ideal.isCoprime_iff_gcd, Perfection.teichmuller₀_spec, Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes, AdicCompletion.factor_eval_eq_evalₐ, Algebra.Generators.exists_presentation_of_free_cotangent, Algebra.IsInvariant.exists_smul_of_under_eq, Ideal.iSup_eq_span, Polynomial.isPrimitive_iff_contentIdeal_eq_top, Ideal.jacobson_eq_top_iff, Algebra.Generators.naive_val, Ideal.Quotient.factorₐ_apply, one_le_primesOver_ncard, RingHom.locally_iff_isLocalization, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors, Module.isTorsionBySet_annihilator, PrimeSpectrum.zeroLocus_span, Ideal.powQuotSuccInclusion_apply_coe, Ideal.map_inf_comap_of_surjective, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq', Submodule.isInternal_prime_power_torsion_of_is_torsion_by_ideal, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, Module.IsTorsionBySet.mk_smul, IsLocalization.mapFrameHom_apply, prod_mem_ideal_map_of_mem_conductor, Ideal.nonempty_minimalPrimes, Ideal.isIdempotentElem_iff_of_fg, AlgebraicGeometry.StructureSheaf.comap_apply, nilradical_le_jacobson, Nat.subset_span_setGcd, Ideal.IsPrime.mul_mem_pow, Ring.KrullDimLE.existsUnique_isPrime, IsAdic.hasBasis_nhds, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, IsAdicComplete.StrictMono.mk_comp_liftRingHom, IsLocalization.map_inf, DoubleQuot.quotQuotToQuotSupₐ_toRingHom, PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal, IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne, Ideal.finrank_quotient_eq_sum, IsLocalization.isMaximal_iff_isMaximal_disjoint, AlgebraicGeometry.IsAffineOpen.ideal_le_iff, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, associatedPrimes.finite, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, IsLocalRing.maximalIdeal_eq_bot, Ideal.Quotient.lift_surjective_of_surjective, Int.card_ideal_quot, AddValuation.self_le_supp_comap, Ideal.relNorm_singleton, Submodule.factor_eq_factor, Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count, Ideal.under_smul, PrimeSpectrum.comap_quotientMk_bijective_of_le_nilradical, HomogeneousIdeal.toIdeal_bot, PowerSeries.map_constantCoeff_le_self_of_X_mem, Ideal.IsPrime.inf_le, Submodule.annihilator_mul, Ideal.map_relNorm, RingHom.eq_liftOfSurjective, Ideal.Quotient.factorₐ_refl, Ideal.map_le_comap_of_inv_on, Polynomial.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, AlgebraicGeometry.Scheme.Hom.liftQuotient_comp, Ideal.eq_bot_or_top, ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, Ideal.IsPrime.inf_le', Algebra.Presentation.naive_relation, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem, Ideal.span_singleton_mul_eq_span_singleton_mul, HomogeneousIdeal.toIdeal_iSup₂, Ideal.comap_sInf', Ideal.inf_mul, Ideal.isTorsionBySet_cotangent, Ideal.isRadical_iInf, Hausdorffification.instIsHausdorff, Ideal.IsPrime.mem_of_pow_mem, ProjectiveSpectrum.union_zeroLocus, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, IsLocalization.AtPrime.exists_algebraMap_quot_eq_of_mem_quot, NumberField.HeightOneSpectrum.adicAbv_def, Ideal.kerLiftAlg_injective, IsDecompositionField.toIsGaloisGroup, Ideal.sup_pow_add_le_pow_sup_pow, Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero, Submodule.IsMinimalPrimaryDecomposition.mem_associatedPrimes, FractionalIdeal.coeIdeal_sup, PrimeSpectrum.vanishingIdeal_eq_top_iff, AddValuation.onQuot_comap_eq, Ideal.relNorm_le_comap, IsNoetherianRing.isClosed_ideal, Ideal.bot_mul, Ideal.sum_ramification_inertia, AdicCompletion.mkₐ_apply_coe, PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radical, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, Ideal.span_singleton_one, FractionalIdeal.finprod_heightOneSpectrum_factorization, Algebra.FormallyUnramified.isField_quotient_map_maximalIdeal, instPosMulStrictMonoIdeal, Ideal.span_eq_top_iff_finite, Ideal.eq_top_of_isUnit_mem, Ideal.radical_inf, Submodule.coe_span_smul, Ideal.pow_succ_lt_pow, Ideal.card_primesOverFinset_le_finrank, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq, Ideal.exists_ideal_over_prime_of_isIntegral_of_isPrime, Ideal.map_mk_comap_factorPow, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, Ring.DimensionLeOne.prime_le_prime_iff_eq, Ideal.span_single_eq_top, Ideal.Quotient.span_singleton_one, normalizedFactorsEquivOfQuotEquiv_symm, ContinuousMap.idealOfSet_closed, Polynomial.contentIdeal_eq_top_of_contentIdeal_mul_eq_top, Submodule.mem_annihilator', Ideal.IsHomogeneous.bot, AdicCompletion.isAdicCauchy_iff, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, Ideal.map_mk_eq_bot_of_le, Ideal.disjoint_powers_iff_notMem, ValuationSubring.idealOfLE_le_of_le, Ideal.IsPrime.multiset_prod_map_le, Ideal.mul_left_self_sup, instWfDvdMonoidIdeal, PrimeSpectrum.sup_vanishingIdeal_le, sub_mem_pNilradical_iff_pow_expChar_pow_eq, IsLocalRing.residue_def, TwoSidedIdeal.orderIsoIsTwoSided_symm_apply, AdicCompletion.val_sum, Polynomial.Monic.quotient_isIntegralElem, PowerSeries.IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top, Ideal.eq_jacobson_iff_sInf_maximal', Pi.ker_ringHom, Algebra.FormallySmooth.comp_lift, FractionalIdeal.le_one_iff_exists_coeIdeal, Ideal.card_stabilizer_eq, Ideal.comap_eq_top_iff, Algebra.TensorProduct.map_ker, isJacobsonRing_iff_sInf_maximal, IsDedekindDomain.HeightOneSpectrum.irreducible, RingHom.mem_ker, Ideal.span_singleton_le_span_singleton, PrimeSpectrum.mem_compl_zeroLocus_iff_notMem, PrimeSpectrum.zeroLocus_radical, RingQuot.idealQuotientToRingQuot_apply, PrimeSpectrum.zeroLocus_minimalPrimes, Ideal.FiniteHeight.eq_top_or_height_ne_top, Ideal.height_le_height_add_of_liesOver, Ideal.IsPrimary.inf, Ideal.stabilizerEquiv_symm_apply_smul, Ideal.mem_span_range_self, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff', Ideal.single_mem_jacobson_matrix, IsHausdorff.iInf_pow_smul, Ideal.iInf_sup_eq_top, PrimeSpectrum.isIrreducible_zeroLocus_iff, IsLocalization.coeSubmodule_bot, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, IsDedekindDomain.exists_forall_sub_mem_ideal, IsDedekindDomain.HeightOneSpectrum.valuation_def, Ideal.isPrimary_finset_inf, ValuativeRel.supp_def, FractionalIdeal.count_ne_zero, Ideal.span_singleton_mul_right_inj, Ideal.IsPrime.smul_iff, Ideal.FG.mul, Ideal.height_le_height_add_one_of_mem, Ideal.le_of_dvd, Ideal.exists_le_prime_disjoint, Ideal.Quotient.mkₐ_toRingHom, RingEquiv.quotientBot_mk, Ideal.image_subset_nonunits_valuationSubring, KaehlerDifferential.End_equiv_aux, Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le, Submodule.mem_annihilator, finrank_quotient_span_eq_natDegree, Ideal.eq_bot_of_comap_eq_bot, Ideal.disjoint_map_primeCompl_iff_comap_le, IsAdicComplete.bot, Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral, PrimeSpectrum.isMin_iff, AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot, nonPrincipals_zorn, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, ValuationSubring.ofPrime_bot, nonPrincipals_eq_empty_iff, Polynomial.map_under_lt_comap_of_weaklyQuasiFiniteAt, Ideal.index_pow_le, Ideal.instFinite, Ideal.IsMaximal.isClosed, FractionalIdeal.coeIdeal_inf, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, MvPolynomial.quotient_map_C_eq_zero, Ideal.iInf_span_singleton_natCast, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff, Polynomial.contentIdeal_eq_top_iff_forall_gaussNorm_eq_one, Ideal.exists_ideal_le_liesOver_of_le, IsLocalization.mk'_mem_iff, ClassGroup.mkMMem_surjective, Ideal.homogeneousHull.gc, Ideal.IsRadical.inf, Submodule.eq_smul_of_le_smul_of_le_jacobson, MvPolynomial.pow_idealOfVars_eq_span, AddMonoidAlgebra.mem_ideal_span_of'_image, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, WittVector.mem_span_p_pow_iff_le_coeff_eq_zero, AlgebraicGeometry.LocallyRingedSpace.coe_toΓSpecSheafedSpace_hom_base_hom_apply_asIdeal, Ideal.mem_of_dvd, AdicCompletion.range_eval, ringKrullDim_quotient_le, Nat.finite_setOf_setGcd_dvd_and_mem_span, Ideal.Quotient.smul_top, Ideal.IsPrime.one_notMem, Ideal.span_singleton_zero, Ideal.multiset_prod_span_singleton, Ideal.comp_quotientMap_eq_of_comp_eq, Ideal.Quotient.eq_zero_iff_dvd, Ideal.mem_of_liesOver, Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat, AdicCompletion.val_neg_apply, Polynomial.gaussNorm_lt_one_iff_contentIdeal_le, Ideal.finite_minimalPrimes_of_isNoetherianRing, smoothSheafCommRing.isUnit_stalk_iff, Ideal.eq_bot_of_minimalPrimes_eq_empty, Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes, Ideal.tensorCotangentHom_tmul, Module.Quotient.mk_smul_mk, RingPreordering.mem_support, Ideal.isMaximal_iff_of_bijective, differentialIdeal_le_iff, Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicComplete, Ideal.sup_pow_eq_top', liftOfDerivationToSquareZero_mk_apply, Ideal.primesOver_bot, Algebra.Extension.Hom.sub_one_tmul, Ideal.ramificationIdx_bot, IsLinearTopology.hasBasis_open_ideal, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff, Ideal.isTwoSided_iff, Ideal.exists_isMaximal_height, Ideal.Quotient.isDomain_iff_prime, Ideal.Factors.isScalarTower, AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff, Ideal.isRadical_bot, Ideal.quotientEquiv_symm_mk, DividedPowers.IsSubDPIdeal.dpow_mem, Algebra.zariskisMainProperty_iff', Perfection.mk_comp_teichmuller', Ideal.Quotient.index_eq_zero, Ideal.radical_bot_of_noZeroDivisors, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, Ring.HasFiniteQuotients.finite_absNorm_le, Ideal.mem_radical_of_pow_mem, Ring.krullDimLE_one_iff, isStronglyTranscendental_mk_radical_conductor, Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes, Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim, Ideal.eq_prime_pow_of_succ_lt_of_le, IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff, IsDiscreteValuationRing.isOpen_iff, instNonUnitalSubsemiringClassIdeal, Ideal.Quotient.nontrivial_iff, isDecompositionField_iff, KaehlerDifferential.D_apply, Algebra.QuasiFinite.iff_finite_primesOver, Ideal.IsHomogeneous.iSup, Ideal.nonPrincipals_zorn, DividedPowers.isDPMorphism_iff, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, IsLocalization.algebraMap_mem_map_algebraMap_iff, Ideal.Quotient.normal, Ideal.Quotient.mk_singleton_self, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Ideal.eq_span_singleton_mul, Ideal.ker_piRingHom_atPrime_eq_of_pure, Algebra.Presentation.naive_relation_apply, mem_conductor_iff, FractionalIdeal.canonicalEquiv_mk0, IsDedekindDomain.primesOverEquivPrimesOver_apply, NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, AdicCompletion.transitionMap_comp_eval, Associates.le_singleton_iff, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical, Ideal.IsPrime.mul_mem_right_iff, Ideal.quotientToQuotientRangePowQuotSucc_mk, Ideal.mem_map_of_equiv, AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff, HomogeneousIdeal.toIdeal_sSup, Submodule.restrictScalars_map_smul_eq, NumberField.FinitePlace.norm_lt_one_iff_mem, Ideal.absNorm_ne_zero_iff, AlgHom.IsArithFrobAt.apply_of_pow_eq_one, Module.support_of_algebra, AdjoinRoot.quotEquivQuotMap_apply, Ideal.mul_sup, KaehlerDifferential.one_smul_sub_smul_one_mem_ideal, Ideal.exists_ideal_liesOver_maximal_of_isIntegral, Ideal.finrank_prime_pow_ramificationIdx, IsSMulRegular.notMem_of_mem_minimalPrimes, Ideal.le_pow_ramificationIdx, AlgebraicGeometry.AffineSpace.spec_le_iff, MaximalSpectrum.range_asIdeal, Ideal.Quotient.stabilizerHom_surjective_of_profinite, Algebra.Extension.Cotangent.mk_eq_zero_iff, Rat.valuation_le_one_iff_den, Algebra.QuasiFiniteAt.exists_basicOpen_eq_singleton, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, Ideal.quotientKerAlgEquivOfRightInverse_symm_apply, Ideal.jacobson_eq_bot, Ideal.mul_mono, Ideal.pi_tensorProductMk_quotient_surjective, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, Ideal.exists_ideal_comap_le_prime, Submodule.annihilator_smul, Submodule.jacobson_smul_lt_top, PrimeSpectrum.mem_zeroLocus, CharacterModule.intSpanEquivQuotAddOrderOf_apply, Ideal.inertia_le_stabilizer, AlgHom.ker_coe_equiv, Ideal.mapCotangent_toCotangent, Ideal.add_mem, Valuation.comap_onQuot_eq, NumberField.RingOfIntegers.ker_algebraMap_eq_bot, IsLocalization.isPrime_iff_isPrime_disjoint, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff, Valuation.pow_Uniformizer_is_pow_generator, SModEq.pow_mul_of_le, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ, Ideal.exists_relNorm_eq_pow_of_isPrime, Localization.localRingHom_id, PrimeSpectrum.subset_vanishingIdeal_zeroLocus, Ideal.Quotient.mk_bijective_iff_eq_bot, Ideal.mem_minimalPrimes_sup, IsDedekindDomain.map_differentIdeal_dvd_differentIdeal, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, IsLocalization.AtPrime.to_map_mem_maximal_iff, Algebra.FormallySmooth.mk_lift, mem_span_C_coeff, AlgHom.toKerIsLocalization_apply, RingHom.lift_injective_of_ker_le_ideal, AdicCompletion.coe_eval, DividedPowers.le_equalizer_of_isDPMorphism, Ideal.IsPrime.le_of_pow_le, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_ofIdealTop, Ideal.mem_sInf, IsPrimitiveRoot.finite_quotient_span_sub_one', Ideal.instIsTwoSidedBot, Nat.mem_maximalIdeal_iff, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, PrimeSpectrum.vanishingIdeal_isIrreducible, Ideal.IsPrime.prod_mem_iff, Ideal.mem_quotient_iff_mem, PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty, QuotientRing.isOpenMap_coe, Ideal.le_map_of_comap_le_of_surjective, IsLocalization.bot_lt_comap_prime, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, PrimeSpectrum.exist_mem_one_of_mem_two, Ideal.pi_le_pi_iff, IsDedekindDomain.inf_pow_eq_prod_of_prime, AdicCompletion.factorₐ_evalₐ_one, Algebra.FormallySmooth.iff_of_surjective, PrimeSpectrum.vanishingIdeal_anti_mono, Algebra.IsInvariant.orbit_eq_primesOver, TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, QuotientRing.isQuotientMap_coe_coe, Ideal.Cotangent.lift_toCotangent, Ideal.quotientKerAlgEquivOfRightInverse_apply, Ideal.add_pow_mem_of_pow_mem_of_le, Ideal.exists_radical_pow_le_of_fg, SModEq.pow_add_one, FractionalIdeal.coeIdeal_le_coeIdeal', PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last, IsPrimitiveRoot.finite_quotient_span_sub_one, AdicCompletion.val_mul, MvPolynomial.mem_pow_idealOfVars_iff', Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors, Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux, Submodule.annihilator_bot, Perfection.coeff_quotientMulEquiv, SModEq.smul', Ideal.Quotient.mk_span_range, minimalPrimes.finite_of_isNoetherianRing, biUnion_associatedPrimes_eq_zero_divisors, IsDomain.minimalPrimes_eq_singleton_bot, associatedPrimes.nonempty, Algebra.PreSubmersivePresentation.naive_toPresentation, Ideal.mem_jacobson_iff, Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge, Polynomial.quotientSpanXSubCAlgEquiv_mk, isFiniteLength_quotient_span_singleton, Module.instFiniteSubtypeMemIdealOfIsNoetherian, Ideal.polynomial_mem_ideal_of_coeff_mem_ideal, instIsAlgebraicQuotientIdealResidueField, DoubleQuot.ker_quotQuotMk, RingOfIntegers.not_dvd_exponent_iff, ringKrullDim_le_ringKrullDim_quotient_add_card, Ideal.sup_mul_right_self, TwoSidedIdeal.asIdeal_jacobson, Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, Ideal.map_eq_bot_iff_of_injective, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq, AdicCompletion.mk_ofAlgEquiv_symm, Ideal.exact_mulQuot_quotOfMul, Ideal.span_singleton_nonZeroDivisors, AdicCompletion.mk_smul_mk, Submodule.top_colon, Ideal.mul_le, IsFractionRing.stabilizerHom_surjective, Submodule.mem_colon_iff_le, TwoSidedIdeal.mem_fromIdeal, IsSemiprimaryRing.isNilpotent, Ideal.span_singleton_eq_top, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux₂, AlgHom.IsArithFrobAt.restrict_injective, Module.FaithfullyFlat.iff_flat_and_ideal_smul_eq_top, AlgebraicGeometry.Scheme.zeroLocus_radical, DoubleQuot.coe_quotQuotEquivQuotSupₐ, associatedPrimes.subset_of_injective, Ideal.IsPrime.mul_notMem, Ideal.quotientMulEquivQuotientProd_snd, StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_bot, WittVector.mem_ker_truncate, LocalSubring.map_maximalIdeal_eq_top_of_isMax, Ideal.height_le_ringKrullDim_quotient_add_one, PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal, Ideal.mem_prime_of_mul_mem_pow, Ideal.dvd_bot, Ideal.mul_add_mem_pow_succ_unique, Polynomial.annIdealGenerator_mem, Ideal.isPrime_map_quotientMk_of_isPrime, Ideal.symm_apply_mem_of_equiv_iff, IsDedekindDomain.HeightOneSpectrum.intAdicAbv_lt_one_iff, RingHom.toKerIsLocalization_apply, Ideal.comap_bot_of_injective, algebraMap_mk, MvPolynomial.monomial_mem_pow_idealOfVars_iff, Ideal.Quotient.stabilizerHom_apply, Ideal.mem_leadingCoeff, Ideal.fst_comp_quotientMulEquivQuotientProd, PrimeSpectrum.zeroLocus_iSup, Ideal.ResidueField.exists_smul_eq_tmul_one, DividedPowers.RatAlgebra.dpow_apply, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, Ideal.span_mul_span', Module.mem_support_iff_exists_annihilator, IsLocalRing.isField_iff_maximalIdeal_eq, Polynomial.mem_annIdeal_iff_aeval_eq_zero, Ideal.finiteHeight_iff, Ideal.homogeneousHull_eq_iSup, Matrix.isRepresentation.toEnd_exists_mem_ideal, isSimpleRing_iff_isTwoSided_imp, FractionalIdeal.num_zero_eq, IsAdic.hasBasis_nhds_zero, LinearMap.annihilator_le_of_injective, IsLocalization.minimalPrimes_comap, AlgebraicGeometry.Scheme.Hom.ideal_ker_le, MaximalSpectrum.equivSubtype_symm_apply_asIdeal, Ring.KrullDimLE.mem_minimalPrimes_iff_le_of_isPrime, Ideal.isRadical_bot_iff, Submodule.IsMinimalPrimaryDecomposition.distinct, AlgebraicGeometry.Scheme.zeroLocus_inf, HomogeneousIdeal.toIdeal_injective, RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev, ideal_eq_bot_of_localization, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_symm_mk, image_comap_zeroLocus_eq_zeroLocus_comap, AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono, Ideal.mul_homogeneous_element_mem_of_mem, AlgebraicGeometry.IsClosedImmersion.spec_of_quotient_mk, Module.annihilator_eq_top_iff, IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime, Ideal.IsTwoSided.mul_mem_of_left, ContinuousMap.AlgHom.closure_ker_inter, Ideal.Quotient.torsionBy_eq_span_singleton, reesAlgebra.monomial_mem, RingHom.pi_bijective_of_isIdempotentElem, PrimeSpectrum.zeroLocus_eq_iff, exists_max_ideal_of_mem_nonunits, Ideal.IsHomogeneous.iInf, Ideal.pow_le_self, Ideal.IsPrime.notMem_of_isCoprime_of_mem, QuotSMulTop.equivQuotTensor_naturality, Ideal.relNorm_algebraMap', Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot, Algebra.Extension.cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Ideal.isCompact_of_fg, ModP.preVal_mk, AdicCompletion.transitionMap_comp_reduceModIdeal, Ideal.mem_matrix, TwoSidedIdeal.mem_asIdealOpposite, FractionalIdeal.coe_one_eq_coeSubmodule_top, RingPreordering.one_notMem_support, Ideal.torsionOf_zero, Ideal.exists_le_prime_notMem_of_isIdempotentElem, Ideal.Quotient.nontrivial, AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule, FractionalIdeal.mem_coeIdeal, isNoetherian_of_liesOver, HomogeneousIdeal.toIdeal_sInf, Ideal.map_quotient_self, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app, IsLocalization.mk'_mem_map_algebraMap_iff, Ideal.ofNat_eq_top, finite_iff_ideal_quotient, Ideal.coe_restrictScalars, Ideal.IsIntegralClosure.comap_lt_comap, Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under, Ideal.mk_mem_cotangentIdeal, Int.quotientSpanEquivZMod_comp_castRingHom, Submodule.coe_mapAlgEquiv_apply, Ideal.relNorm_int, FractionalIdeal.coe_inv_of_ne_zero, IsDecompositionField.rank_right, Ideal.absNorm_dvd_absNorm_of_le, AdicCompletion.ofPowSMul_injective, IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq, conductor_subset_adjoin, Ideal.IsMaximal.mem_pow_mul, MvPolynomial.mk_eq_eval₂, Ideal.pow_right_mono, IsDedekindDomain.HeightOneSpectrum.prime, Algebra.FormallyUnramified.quotient_map, Ideal.isOpen_pow_of_isMaximal, associatedPrimes.eq_singleton_of_isPrimary, Ideal.sum_mem, IsLocalization.coeSubmodule_le_coeSubmodule, Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite, Ideal.iSup_mul, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, Ideal.mem_leadingCoeffNth, Ideal.IsPrime.multiset_prod_le, NumberField.Ideal.tendsto_norm_le_div_atTop₀, FractionalIdeal.coeIdeal_injective, Submodule.finite_quotient_smul, Ideal.Quotient.alg_map_eq, Ideal.setOf_isPrincipal_wellFoundedOn_gt, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, Ideal.Quotient.isUnit_mk_pow_iff_isUnit_mk, Ideal.Filtration.Stable.exists_pow_smul_eq, Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver, IsHausdorff.bot, module_finite_of_liesOver, Ideal.quotientMap_mk, MvPolynomial.pointToPoint_zeroLocus_le, IsLocalization.Away.span_range_mulNumerator_eq_top, AdicCompletion.smul_mk, associatedPrimes.eq_empty_of_subsingleton, FractionalIdeal.coeIdeal_eq_zero', exists_integral_inj_algHom_of_quotient, AdicCompletion.exists_smodEq_pow_add_one_smul, Ideal.isMaximal_iff, Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk, FractionalIdeal.coeIdeal_mul, LocalizedModule.exists_subsingleton_away, Ideal.le_mul_of_no_prime_factors, quotAdjoinEquivQuotMap_apply_mk, Perfection.teichmullerFun_sModEq, Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, MixedCharZero.charP_quotient, Ideal.isRadical_bot_of_noZeroDivisors, Ideal.isPrime_bot, mod_mem_iff, MvPolynomial.zeroLocus_bot, NumberField.HeightOneSpectrum.embedding_mul_absNorm, Ideal.mul_mem_mul, Ideal.matrix_top, Perfection.teichmuller_sModEq, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, Int.absNorm_under_mem, isLinearTopology_iff_hasBasis_ideal, PadicInt.zmodRepr_spec, PrimeSpectrum.vanishingIdeal_union, Ideal.Quotient.lift_mk, Ideal.quotientToQuotientRangePowQuotSucc_surjective, Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, WittVector.ker_map_le_ker_mk_comp_ghostComponent, Ideal.le_comap_of_ramificationIdx_ne_zero, Ideal.span_eq, count_span_normalizedFactors_eq_of_normUnit, IsAdjoinRoot.repr_zero_mem_span, Ideal.comap_mono, coe_subset_nonunits, Ideal.mul_sup_eq_of_coprime_left, instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois, IsLocalization.Away.quotient_of_isIdempotentElem, Ideal.isSimpleOrder, Ideal.zero_eq_bot, Algebra.FormallyUnramified.comp_injective, Ideal.span_singleton_le_iff_mem, Perfection.teichmuller₀_sModEq, Algebra.FinitePresentation.iff, WittVector.fontaineThetaModPPow_teichmuller, factorPowSucc.isUnit_of_isUnit_image, AdicCompletion.pow_smul_top_eq_ker_eval, Submodule.annihilator_top_inter_nonZeroDivisors, Ideal.comap_sInf, AlgHom.IsArithFrobAt.le_comap, Ring.jacobson_le_of_isMaximal, Ideal.le_spanNorm_spanNorm, Ideal.hasBasis_nhds_zero_adic, Ideal.Quotient.factor_surjective, primesOver_finite, Ideal.fg_top, Ideal.idealProdEquiv_symm_apply, Ideal.add_eq_one_iff, Ideal.add_pow_add_pred_mem_of_pow_mem_of_commute, Ideal.homogeneousHull_mono, Ideal.isCancelMulZero, Ideal.iInf_maxPowDividing_eq, Ideal.spanNorm_eq, Ideal.mem_span_singleton_sup, Ideal.finset_inf_span_singleton, pNilradical_eq_bot, FractionalIdeal.exists_mem_algebraMap_eq, FractionalIdeal.absNorm_eq, PowerSeries.IsWeierstrassDivisorAt.isUnit_shift, RingEquiv.idealComapOrderIso_symm_apply, RingTheory.Sequence.isWeaklyRegular_append_iff', Valuation.supp_quot, Ideal.kerLiftAlg_toRingHom, Ideal.map_le_comap_of_inverse, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal, Ideal.relNorm_algebraMap, Rat.HeightOneSpectrum.natGenerator_dvd_iff, Ideal.spanNorm_mul, sectionOfRetractionKerToTensorAux_prop, Submodule.smul_le_right, IsCoprime.sup_eq, OrthogonalIdempotents.surjective_pi, Ideal.ker_tensorProductMk_quotient, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem, Ideal.prod_mono_right, Ideal.nonempty_primesOver, MvPolynomial.mkₐ_eq_aeval, irreducible_pow_sup, Ideal.IsRadical.radical_le_iff, Ideal.natCast_mem_of_charP_quotient, Ideal.Quotient.eq_zero_iff_mem, Ideal.span_mul_span, Ideal.span_one, PrimeSpectrum.isClosed_iff_zeroLocus_ideal, Perfection.teichmuller₀_spec', Ideal.basisSpanSingleton_apply, ringKrullDim_add_length_eq_ringKrullDim_of_isRegular, Submodule.colon_eq_top_iff_subset, AdicCompletion.val_apply_mem_smul_top_iff, tensorKaehlerQuotKerSqEquiv_tmul_D, Ideal.pow_mem_of_mem, Submodule.torsionBySet_ideal_span_singleton_eq, Ideal.exists_ideal_over_prime_of_isIntegral_of_isDomain, ideal_eq_bot_of_localization', Ideal.isPretransitive_of_isGalois, Ideal.coe_smul_primesOver_mk, Algebra.Presentation.relation_mem_ker, Ideal.finrank_quotient_map, Ideal.comap_le_comap_iff_of_surjective, Algebra.Generators.comp_localizationAway_ker, MvPolynomial.mem_map_C_iff, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, derivationToSquareZeroEquivLift_symm_apply_apply_coe, WittVector.ghostComponentModPPow_teichmuller_coeff, Submodule.annihilator_mono, Ideal.Quotient.algEquivOfEqComap_apply, Ideal.exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff, Ideal.iSup_iInf_eq_top_iff_pairwise, Submodule.colon_singleton_zero, Ideal.isCoprime_tfae, RingHom.ker_eq_bot_iff_eq_zero, Ideal.map_sup_comap_of_surjective, Ideal.map_radical_le, Ideal.quotEquivOfEq_eq_factor, RingHom.surjective_localRingHom_of_surjective, Ideal.relNorm_eq_bot_iff, IsAdicComplete.le_jacobson_bot, DividedPowers.SubDPIdeal.inf_carrier_def, DividedPowers.IsSubDPIdeal.isSubideal, Ideal.map_bot, Ideal.quotientKerAlgEquivOfSurjective_apply, Ideal.le_toIdeal_homogeneousHull, DoubleQuot.quotQuotMkₐ_toRingHom, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, not_dvd_differentIdeal_of_isCoprime_of_isSeparable, MaximalSpectrum.equivSubtype_apply_coe, Ideal.inf_eq_mul_of_pure, Ideal.ker_quotient_lift, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, DividedPowers.SubDPIdeal.sSup_carrier_def, NumberField.FinitePlace.norm_def_int, Ideal.exists_forall_sub_mem_ideal, Valuation.leIdeal_v_le_of_mem, Polynomial.coeff_mem_pow_of_mem_adjoin_C_mul_X, Ring.HasFiniteQuotients.finite_setOf_mem, Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, IsFractionRing.coeSubmodule_le_coeSubmodule, Ideal.mem_of_one_mem, Submodule.torsionBySet_isInternal, Ideal.IsPrime.mem_or_mem, AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact, Ideal.exists_ideal_lt_liesOver_of_lt, RingHom.liftOfRightInverse_comp_apply, Algebra.Smooth.exists_span_eq_top_isStandardSmooth, Ideal.card_norm_le_eq_card_norm_le_add_one, Ideal.height_le_ringKrullDim_quotient_add_encard, PrimeSpectrum.exists_primeSpectrum_prod_le, Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx, RingHom.prod_bijective_of_isIdempotentElem, Ideal.coe_toTwoSided, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, RingHom.quotientKerEquivOfRightInverse.Symm.apply, IsLocalization.AtPrime.equivQuotMaximalIdeal_apply_mk, cardQuot_pow_of_prime, AdicCompletion.Ideal.mk_eq_mk, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime, Ideal.iInf_span_singleton, Ideal.IsPrime.mul_le, Module.isTorsionBySet_iff_is_torsion_by_span, Polynomial.jacobson_bot_of_integral_localization, Ideal.map_sup, Polynomial.Monic.leadingCoeff_notMem, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, LinearMap.reduceModIdeal_apply, Valuation.Integers.maximalIdeal_eq_setOf_le_v_algebraMap, RingTheory.Sequence.isWeaklyRegular_append_iff, Ideal.isPretransitive_of_isGaloisGroup, dvd_differentIdeal_iff, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors, Ideal.prod_mono, Algebra.IsSmoothAt.exists_notMem_smooth, AdjoinRoot.quotEquivQuotMap_apply_mk, Ideal.IsTwoSided.instHPowNat, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, transcendental_iff_ker_eq_bot, Ideal.comap_map_quotientMk, Algebra.FormallySmooth.exists_lift, Localization.exists_awayMap_bijective_of_residueField_surjective, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, PrimeSpectrum.vanishingIdeal_empty, DividedPowers.isSubDPIdeal_sup, Ideal.minimalPrimes_eq_comap, Submodule.IsPrimary.radical_colon_singleton_eq_ite, Ideal.prod_eq_top_iff, Submodule.torsionBy.mk_ideal_smul, HomogeneousIdeal.toIdeal_top, Ideal.Quotient.mkₐ_ker, PrimeSpectrum.zeroLocus_bot, AdicCompletion.ofPowSMul_val_apply_eq_zero, mem_primesOverFinset_iff, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, DividedPowers.DPMorphism.ideal_comp, Submodule.instFiniteQuotientIdealHSMulTop, Ideal.pow_le_pow_right, Ideal.radical_eq_sInf, Ideal.Quotient.mk_surjective, Ideal.IsLocal.le_jacobson, DividedPowers.isDPMorphism_def, FractionalIdeal.coeIdeal_eq_one, IsCyclotomicExtension.Rat.galEquivZMod_stabilizer, Ideal.prod_mem_prod, Ideal.Quotient.eq, Ideal.quotientEquivAlgOfEq_mk, Ideal.IsHomogeneous.isPrime_iff, diffToIdealOfQuotientCompEq_apply, Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge, Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective, Ideal.eq_jacobson_iff_notMem, Ideal.exists_minimalPrimes_le, Ideal.comap_surjective_of_faithfullyFlat, RingHom.surjectiveOnStalks_iff_forall_maximal', Ideal.top_liesOver_top, RingHom.quotientKerEquivOfSurjective_apply_mk, Ideal.IsPrime.multiset_prod_mem_iff_exists_mem, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, Ideal.span_singleton_mul_span_singleton, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, Polynomial.Monic.finite_quotient, AlgebraicGeometry.Scheme.IdealSheafData.ideal_top, Ideal.map_eq_top_iff, Valued.integer.coe_span_singleton_eq_closedBall, Ideal.IsPrime.mem_or_mem_of_mul_eq_zero, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson, PadicInt.mem_span_pow_iff_le_valuation, instLiesOverResidueFieldBotIdeal, CharP.quotient', Algebra.Extension.Hom.mapKer_apply_coe, Submodule.IsMinimalPrimaryDecomposition.injOn, NumberField.discr_mem_differentIdeal, Perfection.mk_comp_teichmuller, PrimeSpectrum.range_comap_snd, idealFactorsEquivOfQuotEquiv_symm, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply, Ideal.injective_lift_iff, Ideal.sup_mul_inf, Ideal.map_iSup_comap_of_surjective, Ideal.ker_le_comap, Algebra.Extension.contangentEquiv_tmul, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul, Ideal.quotOfMul_surjective, AlgebraicClosure.le_maxIdeal, Ideal.add_mem_iff_right, Ideal.primesOver.liesOver, IsPRadical.ker_le, ClassGroup.mk_mk0, Ideal.Quotient.factor_ker, IsPrecomplete.top, Algebra.Generators.cMulXSubOneCotangent_eq, ValuationSubring.coe_mem_nonunits_iff, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, Ideal.pointwise_smul_eq_comap, Ideal.map_le_iff_le_comap, Ideal.toCotangent_apply, Ideal.snd_comp_quotientMulEquivQuotientProd, Ideal.isDomain, Polynomial.isEisensteinAt_iff, Ideal.Quotient.isScalarTower_of_liesOver, NumberField.absNorm_differentIdeal, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, Ideal.ramificationIdx_bot', DoubleQuot.ker_quotLeftToQuotSup, Ideal.homogeneousCore'_le, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq, ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring, Algebra.FormallySmooth.comp_surjective, Ideal.finite_mulSupport_coe, Algebra.IsEtaleAt.exists_isStandardEtale, ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal, Submodule.isPrimary_decomposition_pairwise_ne_radical, Perfection.teichmuller_zero, PrimeSpectrum.zeroLocus_mul, Ideal.comap_map_of_surjective, Ideal.mem_normalizedFactors_iff, Ideal.matrix_jacobson_le, Ideal.eq_top_iff_one, isSimpleModule_iff_quot_maximal, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, Ideal.annihilator_quotient, Ideal.absNorm_top, Ideal.Factors.liesOver, Ideal.absNorm_apply, ProjectiveSpectrum.zeroLocus_bot, IsAdicComplete.mk_liftAlgHom, Algebra.FormallyEtale.iff_comp_bijective, Ideal.absNorm_pos_of_nonZeroDivisors, AlgebraicGeometry.Scheme.eq_zeroLocus_of_isClosed_of_isAffine, Ideal.coe_comap, Ideal.quotientEquiv_apply, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, Ideal.quotientInfEquivQuotientProd_snd, Ideal.toCotangent_eq_zero, AssociatePrimes.mem_iff, Ideal.Filtration.pow_smul_le_pow_smul, Ideal.mul_unit_mem_iff_mem, AdicCompletion.pow_smul_top_le_ker_eval, IsAdicComplete.mkₐ_comp_liftAlgHom, Ideal.pow_mem_of_pow_mem, associatedPrimes.prod, Ideal.eq_top_of_unit_mem, Ideal.mul_assoc, IsLocalization.AtPrime.mem_primesOver_of_isPrime, IsDedekindDomain.inf_prime_pow_eq_prod, KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, Ideal.zero_mem, Ideal.isCoprime_iff_exists, Ideal.radical_eq_jacobson_iff_radical_quotient_eq_jacobson_bot, Ideal.mem_primeCompl_iff, DividedPowers.SubDPIdeal.dpow_mem, Ring.DirectLimit.quotientMk_of, IsSemiprimaryRing.isSemisimpleRing, Ideal.cotangentEquivIdeal_apply, Ideal.instIsTwoSidedIInf, Ideal.comap_map_mk, Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt, AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply, exists_maximalIdeal_pow_eq_of_principal, Ideal.exists_subset_radical_span_sup_of_subset_radical_sup, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ, PadicInt.norm_le_pow_iff_mem_span_pow, FractionalIdeal.coeIdeal_bot, Ideal.sum_pow_mem_span_pow, coe_toIdeal, Ideal.apply_mem_of_equiv_iff, Basis.mem_ideal_iff', Ideal.quotientToQuotientRangePowQuotSucc_injective, Algebra.idealMap_isLocalizedModule, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff, Ideal.minimalPrimes_map_of_surjective, PrimeSpectrum.closure_image_comap_zeroLocus, Submodule.range_powSMulQuotInclusion, RingHom.one_notMem_ker, sectionOfRetractionKerToTensor_algebraMap, Ideal.IsHomogeneous.sSup, exists_leadingCoeff_pow_smul_mem_radical_conductor, Ideal.associatesEquivIsPrincipal_symm_apply, Ideal.IntegralClosure.eq_bot_of_comap_eq_bot, Ideal.adic_basis, Ideal.stableFiltration_N, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal', count_le_of_ideal_ge, Int.ringChar_idealQuot, Ideal.add_pow_add_pred_mem_of_pow_mem, EqualCharZero.nonempty_algebraRat_iff, Ideal.norm_mem_spanNorm, IsInertiaField.rank_right, Algebra.Extension.Cotangent.mk_eq_mk_iff_sub_mem, IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff, Polynomial.mem_iff_annIdealGenerator_dvd, associated_norm_prod_smith, Ideal.Quotient.ringHom_ext_iff, Ring.HasFiniteQuotients.finite_cardQuot_le, RingHom.pNilradical_le_ker_of_perfectRing, Ideal.constr_basisSpanSingleton, Module.isTorsionBySet_annihilator_top, Localization.exists_awayMap_injective_of_localRingHom_injective, Ideal.apply_coe_mem_map, Ideal.pow_sup_eq_top', dvd_differentIdeal_of_not_isSeparable, PrimeSpectrum.closure_singleton, Ideal.iInf_ker_le, Ideal.exists_maximal_not_isPrincipal, Ideal.mem_map_C_iff, Ideal.finite_mulSupport, TensorProduct.quotTensorEquivQuotSMul_symm_mk, Ring.not_isField_iff_exists_prime, Ideal.iInf_pow_eq_bot_of_isLocalRing, Ideal.IsPrime.smul, IsLocalRing.not_isLocalRing_tfae, toIdeal_le_toIdeal_iff, DividedPowers.isSubDPIdeal_ker, PrimeSpectrum.coe_primesOverOrderIsoFiber_apply_asIdeal, AlgebraicGeometry.IsClosedImmersion.Spec_iff, Ideal.span_singleton_mul_left_mono, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Int.absNorm_under_dvd_absNorm, ringKrullDim_le_ringKrullDim_add_card, RingHom.kerLift_injective, Ideal.IsHomogeneous.inf, UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime, Ideal.exists_isPrime_liesOver_of_faithfullyFlat, Valuation.leIdeal_mono, Ideal.mul_add_mem_pow_succ_inj, Ideal.Quotient.isDomain, Ideal.comap_lt_comap_of_integral_mem_sdiff, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, IsArtinianRing.mem_minimalPrimes, AdicCompletion.evalOneₐ_of, Ideal.mem_iInf, AlgebraicGeometry.stalkwise_Spec_map_iff, IsFractionRing.stabilizerHom_apply_apply_mk, Algebra.FormallySmooth.iff_split_surjection, AlgebraicGeometry.Scheme.default_asIdeal, Valuation.leIdeal_zero, Ideal.Quotient.mk_out, Ideal.eq_bot_of_prime, instIsArtinianRingQuotientIdeal, Submodule.torsionBySet_le_torsionBySet_pow, ProjectiveSpectrum.gc_ideal, Ideal.IsTwoSided.mul_one, HomogeneousIdeal.toIdeal_sup, Ring.jacobson_le_of_eq_bot, Ideal.restrictScalars_mul, Ideal.jacobson_mono, Ideal.jacobson_eq_iff_jacobson_quotient_eq_bot, Ideal.sup_mul_eq_of_coprime_right, AdicCompletion.val_add, Ideal.not_isPrime_iff, Ideal.pow_sup_pow_eq_top', Ideal.subset_union_prime_finite, Algebra.trace_quotient_mk, Ideal.IsMaximal.mul_mem_pow, Ideal.IsMaximal.out, IsNoetherianRing.isNilpotent_nilradical, Ideal.primeHeight_eq_zero_iff, RingHom.liftOfRightInverse_comp, RingHom.injective_iff_ker_eq_bot, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, Ideal.smul_mem_pointwise_smul, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, KaehlerDifferential.D_tensorProductTo, Ideal.mul_le_left, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, Ring.KrullDimLE.isNilpotent_iff_mem_maximalIdeal, IsDedekindDomain.HeightOneSpectrum.intValuation_def, Ideal.mem_span, Ideal.IsPrime.pow_le_iff, Ideal.isIdempotentElem_of_pure, ContinuousMap.ideal_gc, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf, Ideal.mem_span_range_iff_exists_fun, MvPolynomial.quotient_mk_comp_C_injective, QuotSMulTop.equivQuotTensor_naturality_mk, Ideal.radical_le_radical_iff, ValuationRing.iff_ideal_total, Ideal.isPrime_nat_iff, AlgebraicClosure.Monics.map_eq_prod, liftOfDerivationToSquareZero_apply, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, Ideal.associatesEquivIsPrincipal_apply, Algebra.Extension.Cotangent.mk_surjective, Algebra.exists_formallyUnramified_of_isUnramifiedAt, Polynomial.contentIdeal_eq_bot_iff, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, isLinearTopology_iff_hasBasis_open_ideal, TwoSidedIdeal.top_asIdeal, AdicCompletion.val_one, Ideal.quotientMap_injective', Ideal.exists_mul_add_sub_mem_of_mem_jacobson, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map, Ring.KrullDimLE.minimalPrimes_eq_setOf_isMaximal, PrimeSpectrum.gc_set, mem_pNilradical, IsLocalization.orderIsoOfPrime_symm_apply_coe, Ideal.prime_iff_isPrime, Ideal.bot_isMaximal, TwoSidedIdeal.mem_asIdeal, Submodule.mem_smul_top_iff, Ideal.span_range_pow_eq_top, ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom, ProjectiveSpectrum.zeroLocus_anti_mono_ideal, ContinuousMap.setOfTop_eq_univ, IsAdicComplete.mk_liftRingHom, Algebra.TensorProduct.tensorQuotientEquiv_symm_apply_tmul, Ideal.coprime_of_no_prime_ge, Submodule.exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot, Ideal.quotientEquivAlg_symm, Submodule.mem_annihilator_span, IsArtinianRing.isNilpotent_jacobson_bot, DividedPowers.span_isSubDPIdeal_iff, AlgHom.IsArithFrobAt.card_pos, AdicCompletion.factor_eval_liftRingHom, Ideal.asIdeal_toTwoSided, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul, RingHom.IsIntegral.quotient, Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_root_of_monic_mem, Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite, Ideal.span_singleton_mul_right_mono, Algebra.Extension.Hom.subToKer_apply_coe, IsLocalRing.primesOverFinset_eq, nonPrincipals_def, Module.annihilator_eq_bot, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, Ideal.sup_iInf_eq_top, Algebra.Generators.ofComp_kerCompPreimage, Ideal.isCompactElement_top, dividedPowersBot_dpow_eq, IsLocalization.disjoint_comap_iff, Ideal.finite_factors, not_dvd_differentIdeal_of_isCoprime, Polynomial.contentIdeal_zero, Ideal.Factors.finrank_pow_ramificationIdx, NumberField.exists_ideal_in_class_of_norm_le, PerfectRing.pNilradical_eq_bot, Ideal.mem_inf, PrimeSpectrum.nilradical_eq_iInf, DividedPowers.Quotient.isDPMorphism, Ideal.quotientMulEquivQuotientProd_fst, Ideal.instLiesOverBotOfIsPrime, Ring.KrullDimLE.mem_minimalPrimes_iff, Polynomial.coeff_mem_radical_span_coeff_of_dvd, MonoidAlgebra.mem_ideal_span_of_image, Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_is_extension, Perfection.coe_teichmuller_eq_teichmuller₀, Ideal.mem_iInf_smul_pow_eq_bot_iff, Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, IsPrimitiveRoot.card_quotient_toInteger_sub_one, Ideal.instNontrivial, Ideal.Filtration.pow_smul_le, DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ, Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors, Hausdorffification.lift_comp_of, isNilpotent_tensor_residueField_iff, Algebra.weaklyQuasiFiniteAt_iff, Ideal.rank_pow_quot_aux, NumberField.Ideal.tendsto_norm_le_div_atTop, RingHom.ker_eq_comap_bot, Ideal.primesOver.isPrime, Module.annihilator_pi, DividedPowers.isSubDPIdeal_iSup, Ideal.Quotient.mkₐ_eq_mk, Ideal.irreducible_of_irreducible_absNorm, Ideal.rootsOfUnityMapQuot_apply, Ideal.IntegralClosure.comap_lt_comap, Module.associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimes, StandardEtalePresentation.toPresentation_σ', Submodule.colon_mono, FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal, not_dvd_differentIdeal_iff, TrivSqZeroExt.kerIdeal_sq, map_nonunit, Ideal.ofList_append, Ideal.homogeneousCore'_eq_sSup, Ideal.smul_restrictScalars, Ideal.mem_primesOver_iff_mem_normalizedFactors, Module.IsTorsionBySet.isScalarTower, Ideal.mul_mem_right, Ideal.map_sInf, instNonUnitalSubringClassIdeal, Ideal.count_associates_eq, Ideal.cotangentToQuotientSquare_injective, aeval_derivative_mem_differentIdeal, Perfection.exists_teichmullerFun, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus, Submodule.mem_smul_span, AdicCompletion.evalₐ_liftAlgHom, AdicCompletion.surjective_evalₐ, Ideal.ne_top_iff_exists_maximal, Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map, Ideal.natAbs_det_equiv, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, Submodule.torsion_gc, MvPolynomial.vanishingIdeal_empty, Ideal.torsionOf_eq_top_iff, Ideal.FG.isNilpotent_iff_le_nilradical, Ideal.coe_smul_primesOver_eq_map_galRestrict, WittVector.quotientPEquiv_mk, Ideal.isOpen_of_isOpen_subideal, Ideal.map_algebraMap_eq_finset_prod_pow, instIsIntegralQuotientIdeal, AlgebraicGeometry.Scheme.zeroLocus_biInf_of_nonempty, Ideal.absNorm_eq_one_iff, AlgEquiv.prodQuotientOfIsIdempotentElem_apply_snd, AdicCompletion.transitionMap_map_pow, IsLocalRing.le_maximalIdeal, Submodule.powSMulQuotInclusion_mk, idealFactorsEquivOfQuotEquiv_is_dvd_iso, isAssociatedPrime_iff_exists_injective_linearMap, Ideal.Quotient.ker_stabilizerHom, Ideal.rank_pow_quot, Ideal.subtype_isoBaseOfIsPrincipal_eq_mul, EqualCharZero.iff_not_mixedCharZero, Algebra.exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ, IsAssociatedPrime.annihilator_le, Ideal.minimal_primes_comap_of_surjective, Ideal.map_height_le_one_of_mem_minimalPrimes, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, Ideal.instIsTwoSidedTop, DoubleQuot.quotQuotEquivQuotSup_quotQuotMk, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, isArtinianRing_iff_isNilpotent_maximalIdeal, ProjectiveSpectrum.ideal_le_vanishingIdeal_zeroLocus, NumberField.torsionOrder_dvd_absNorm_sub_one, Module.associatedPrimes.mem_associatedPrimes_atPrime_of_mem_associatedPrimes, Submodule.exists_isInternal_prime_power_torsion, Algebra.Extension.tensorCotangentInvFun_smul_mk, Ideal.radical_pow, Submodule.mul_smul, AlgebraicGeometry.Spec.coe_toTop_map_hom_apply_asIdeal, count_span_normalizedFactors_eq, IsArtinianRing.exists_not_mem_forall_mem_of_ne, Ideal.exists_mul_add_mem_pow_succ, Basis.mem_ideal_iff, Module.IsTorsionBySet.isSemisimpleModule_iff, Algebra.Generators.ker_comp_eq_sup, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, Ideal.pi_mkQ_rTensor, Ideal.le_comap_map, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_subset_zeroLocus, Ideal.quotientKerAlgEquivOfSurjective_symm_apply, support_of_supportDim_eq_zero, span_singleton_inf_span_singleton, Ideal.quotientKerAlgEquivOfSurjective_mk, Submodule.factorPow_comp_powSMulQuotInclusion, Ideal.Quotient.nontrivial_of_liesOver_of_ne_top, Ideal.mem_quotient_iff_mem_sup, Ideal.minimalPrimes_eq_subsingleton_self, Ideal.comap_minimalPrimes_eq_of_surjective, Ideal.span_singleton_mem_isPrincipalSubmonoid, Ideal.mem_torsionOf_iff, AdicCompletion.val_sub, IsHausdorff.eq_iff_smodEq, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, Ideal.span_eq_bot, AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval, Ideal.smul_bot, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk, Ideal.hasFiniteMulSupport, Valuation.Integers.isPrincipal_iff_exists_eq_setOf_valuation_le, DoubleQuot.quotQuotEquivCommₐ_toRingEquiv, DoubleQuot.coe_quotQuotToQuotSupₐ, Ideal.Quotient.norm_mk_lt, Algebra.exists_etale_of_isEtaleAt, Ideal.radical_le_jacobson, Ideal.range_finsuppTotal, Valuation.onQuot_comap_eq, Ideal.span_zero, AlgEquiv.quotientBot_symm_mk, Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top, Ideal.ofList_nil, IsDiscreteValuationRing.TFAE, IsLocalRing.basisQuotient_apply, Ideal.torsionMapQuot_injective, biUnion_associatedPrimes_eq_compl_nonZeroDivisors, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, Ideal.factors_span_eq, Perfection.teichmuller_eq_teichmuller₀_toMonoidHom, HomogeneousIdeal.toIdeal_iInf₂, Ideal.primaryComponent_mem, IsCoprime.exists, RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial, Ideal.injective_algebraMap_quotient_residueField, Submodule.sup_torsionBySet_ideal_eq_torsionBySet_inf, Submodule.instIsPrimeValIdealMemSetAssociatedPrimes, Algebra.Generators.naive_σ, IsPrimitiveRoot.idealQuotient_mk, Ideal.Quotient.isUnit_mk_pow_iff_notMem, mem_minimalPrimes_of_primeHeight_eq_height, Ideal.IsMaximal.coprime_of_ne, NumberField.FinitePlace.norm_eq_one_iff_notMem, Ideal.unit_mul_mem_iff_mem, trace_quotient_eq_trace_localization_quotient, Ideal.map_eq_iff_sup_ker_eq_of_surjective, Ideal.top_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem, FractionalIdeal.coeIdeal_eq_zero, AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_supportSet, Ideal.quotientEquiv_mk, Ideal.add_eq_sup, Ideal.coe_closure, Ideal.quotientMap_surjective, Ideal.inertiaDeg_bot, IsPrecomplete.prec, Algebra.Extension.Hom.sub_aux, FractionalIdeal.instPosMulReflectLEIdealOfIsDedekindDomain, AdicCompletion.val_neg, Ideal.ker_quotientMap_mk, Ideal.comap_le_map_of_inv_on, Ideal.ringJacobson_le_jacobson, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, Polynomial.IsEisensteinAt.mem, Ideal.isUnit_iff, Ideal.Quotient.algebra_isIntegral_of_liesOver, Ideal.powQuotSuccInclusion_injective, IsLocalRing.CotangentSpace.map_eq_top_iff, Submodule.smul_comap_le_comap_smul, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection, Ideal.pointwise_smul_le_pointwise_smul_iff, Ideal.radical_iInf_le, IsLocalRing.isOpen_maximalIdeal_pow, Ideal.le_comap_pow, Ideal.prod_span, Ideal.associatesEquivIsPrincipal_mul, Submodule.isInternal_prime_power_torsion, DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv, IsDiscreteValuationRing.iff_pid_with_one_nonzero_prime, Ideal.map_inf_le, PrimeSpectrum.stableUnderGeneralization_singleton, Ideal.sub_mem, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, Ideal.iInf_pow_eq_bot_of_isDomain, Ideal.mem_map_iff_of_surjective, Algebra.trace_quotient_eq_of_isDedekindDomain, Ideal.quotient_map_comp_mkₐ, exists_leadingCoeff_pow_smul_mem_conductor, StandardEtalePair.aeval_X_g_mul_mk_X, AdicCompletion.transitionMap_ideal_mk, idealFactorsFunOfQuotHom_id, Ideal.mul_le_inf, instMulPosStrictMonoIdeal, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, Ideal.isCoprime_biInf, ClassGroup.exists_mk0_eq_mk0, Ideal.Quotient.smulCommClass', Ideal.spanNorm_bot, RingHom.ker_coe_equiv, instIsSimpleOrderIdeal, Ideal.map_iInf_comap_of_surjective, Ideal.finite_quotient_pow, derivationOfSectionOfKerSqZero_apply_coe, instIsScalarTowerQuotientIdealResidueField, Ideal.card_stabilizer_eq_card_inertia_mul_finrank, AdicCompletion.transitionMap_map_mul, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk, Ideal.span_mono, Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, sectionOfRetractionKerToTensorAux_algebraMap, IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotient, MvPolynomial.C_mem_pow_idealOfVars_iff, Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, Ideal.quotientInfToPiQuotient_mk', IsPrecomplete.prec', nilpotent_iff_mem_prime, Ideal.zeroLocus_inj_of_pure, IsDedekindDomain.primesOverEquivPrimesOver_symm_apply, Ideal.le_ker_atPrime_of_forall_exists_eq_mul, AlgEquiv.prodQuotientOfIsIdempotentElem_apply_fst, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono, nilradical_eq_bot_iff, Ideal.ofList_cons_smul, Ideal.Quotient.mk_eq_mk, Algebra.mem_ideal_map_adjoin, image_specComap_zeroLocus_eq_zeroLocus_comap, Ideal.sup_mul_eq_of_coprime_left, Ideal.finprod_count, AlgebraicGeometry.Scheme.zeroLocus_span, Ideal.nonempty_inter_nonZeroDivisors_of_faithfulSMul, ClassGroup.mk0_surjective, AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup, Ideal.exists_coeff_ne_zero_mem_comap_of_root_mem, Submodule.iInf_colon, DividedPowers.SubDPIdeal.memCarrier, Ideal.mul_iSup, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, Ideal.add_pow_mem_of_pow_mem_of_le_of_commute, Ideal.quotEquivOfEq_symm, Ideal.disjoint_primeCompl_of_liesOver, Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul, Perfection.mk_teichmuller₀, Ideal.IsPrime.exists_mem_prime_of_ne_bot, Ideal.colon_span, Algebra.Generators.cotangentRestrict_mk, Ideal.jacobson_bot_polynomial_of_jacobson_bot, Ideal.coe_piOrderIso_symm_apply, Ideal.Quotient.instRingHomSurjectiveQuotientMk, Irreducible.maximalIdeal_eq_closedBall, PrimeSpectrum.coe_vanishingIdeal, Ideal.finite_setOf_absNorm_le, Submodule.smul_le_of_le_smul_of_le_jacobson_bot, Ideal.jacobson_top, Ideal.mul_mem_mul_rev, Ideal.sup_height_eq_ringKrullDim, Ideal.IsHomogeneous.top, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk, CharP.quotient, Algebra.Generators.H1Cotangent.δ_eq_δAux, Ideal.radicalInfTopHom_apply, Ideal.prod_eq_bot_iff, Ideal.map_surjective_of_surjective, Hausdorffification.lift_of, Submodule.AssociatePrimes.mem_iff, Submodule.iInf_colon_iUnion, TwoSidedIdeal.gc, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, Ideal.pow_right_strictAnti, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count, Ideal.minimalPrimes_comap_subset, Algebra.FormallyUnramified.quotient, Ideal.sup_prod_eq_top, DividedPowers.IsSubDPIdeal.dpow_eq, Ideal.exists_mul_sub_mem_of_sub_one_mem_jacobson, Ideal.mem_span_pair, isLocalHom_of_le_jacobson_bot, Ideal.isRadical_iff_pow_one_lt, Ideal.pointwise_central_scalar, Ideal.span_empty, Ideal.quotientInfToPiQuotient_mk, Ideal.exists_mem_pow_notMem_pow_succ, Ideal.finiteHeight_iff_lt, FractionalIdeal.exists_eq_spanSingleton_mul, derivationToSquareZeroEquivLift_apply_coe_apply, Ideal.spanNorm_le_comap, Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, Module.support_eq_zeroLocus, mem_reesAlgebra_iff, Ideal.span_singleton_mul_left_inj, IdealFilter.IsGabriel.gabriel_closed, Ideal.span_singleton_lt_span_singleton, AlgHom.ker_kerSquareLift, IsAdicComplete.StrictMono.factorPow_comp_extend, Ideal.homogeneousCore'_mono, Ideal.matrix_strictMono_of_nonempty, Ideal.exists_ideal_over_maximal_of_isIntegral, height_le_ringKrullDim_quotient_add_spanFinrank, Ideal.add_mem_iff_left, Polynomial.map_under_lt_comap_of_quasiFiniteAt, Ideal.mem_isPrincipalSubmonoid_iff, Ideal.uniqueFactorizationMonoid, Ideal.span_singleton_absNorm, Ideal.map_sSup, Ideal.exists_le_maximal, liftOfDerivationToSquareZero_mk_apply', Submodule.FG.jacobson_smul_lt, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count, Ideal.quotientInfEquivQuotientProd_fst, Ideal.univ_eq_iUnion_image_add, Ideal.pointwise_smul_toAddSubgroup, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, PrimeSpectrum.basicOpen_le_basicOpen_iff, nilradical_eq_sInf, Ideal.mem_mul_span_singleton, Ideal.isCoprime_span_singleton_iff, ContinuousMap.mem_setOfIdeal, Algebra.FormallySmooth.exists_adicCompletionEvalOneₐ_comp_eq, Ideal.IsTwoSided.pow_add, Ideal.quotientMap_algebraMap, DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv, Algebra.FormallyUnramified.iff_comp_injective, ClassGroup.exists_min, WittVector.quotEquivOfEq_ghostComponentModPPow, AdicCompletion.evalₐ_of, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_comp_asIdeal, PrimeSpectrum.mem_basicOpen, Algebra.IsUnramifiedAt.exists_notMem_forall_ne_mem_and_adjoin_eq_top, IsLocalRing.CotangentSpace.span_image_eq_top_iff, Ideal.Quotient.isNoetherianRing, AdjoinRoot.quotEquivQuotMap_symm_apply, isPrecomplete_iff, IsLocalRing.notMem_maximalIdeal, CompleteOrthogonalIdempotents.bijective_pi', Ideal.isPrime_iff, PowerSeries.isWeierstrassDivisionAt_iff, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, StandardEtalePresentation.toPresentation_val, Polynomial.isWeaklyEisensteinAt_iff, AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, Ideal.isDomain_map_C_quotient, NumberField.mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap, Ideal.coe_prod, Ideal.map_mono, Ideal.height_le_height_add_encard_of_subset, Polynomial.contentIdeal_mul_eq_top_of_contentIdeal_eq_top, MvPolynomial.zeroLocus_top, PrimeSpectrum.subset_zeroLocus_vanishingIdeal, PrimeSpectrum.exist_mem_one_of_mem_maximal_ideal, Ideal.eq_top_of_norm_lt_one, Ring.HasFiniteQuotients.finiteQuotient, Ideal.lcm_eq_inf, Ideal.neg_mem_iff, Ideal.isCoprime_iff_add, DividedPowers.Quotient.dpow_apply, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, conductor_mul_differentIdeal, Ideal.Quotient.mk_eq_one_iff_sub_mem, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, MvPolynomial.mem_ideal_span_monomial_image_iff_dvd, Ideal.eq_prime_pow_mul_coprime, Algebra.instEssFiniteTypeQuotientIdeal, ProjectiveSpectrum.zeroLocus_sup_ideal, IsSMulRegular.subsingleton_linearMap_iff, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, Module.annihilator_dfinsupp, Ideal.radical_top, Ideal.mem_minimalPrimes_iff_isPrime, FractionalIdeal.map_canonicalEquiv_mk0, Ideal.mul_mono_left, IsSemisimpleRing.jacobson_eq_bot, Submodule.mem_colon_singleton, Ideal.comap_top, Perfection.coeff_zero_symm_quotientMulEquiv, Ideal.absNorm_eq_pow_inertiaDeg, Algebra.Extension.Hom.sub_tmul, ContinuousMap.idealOfEmpty_eq_bot, topologicalRing_quotient, Ideal.quotientMap_injective, IsAdicComplete.mk_lift, Submodule.finrank_quotient_eq_sum, AdicCompletion.evalOneₐ_surjective, Ideal.prod_top_top, Ideal.map_top, Submodule.top_smul, Ideal.eq_top_iff_of_liesOver, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, Module.isTorsionBySet_iff_subset_annihilator, Ideal.minimalPrimes_eq_empty_iff, AdicCompletion.factor_evalₐ_eq_eval, instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree, AddValuation.mem_supp_iff, isStronglyTranscendental_mk_of_mem_minimalPrimes, Ideal.mul_iInf, Ideal.spanNorm_mul_spanNorm_le, Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisors, Ideal.mem_span_insert, Ideal.isPrimary_iff, AdicCompletion.evalₐ_comp_liftRingHom, PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal, Ideal.Factors.finiteDimensional_quotient_pow, Submodule.span_smul_eq, AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le, Ideal.cotangentEquivIdeal_symm_apply, Submodule.mem_colon, Ideal.Quotient.smulCommClass, Ideal.finprod_heightOneSpectrum_factorization_coe, Ideal.IsPrime.mul_mem_left_iff, pNilradical_one, RingHom.quotientKerEquivOfRightInverse.apply, DividedPowers.SubDPIdeal.sup_carrier_def, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, Ideal.map_le_of_le_comap, Ideal.instNoZeroDivisors, Ideal.eq_inf_of_isPrime_inf, Ideal.Quotient.liftₐ_apply, Ideal.mem_radical_iff, Ideal.IsPrime.mem_or_mem', AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, isJacobsonRing_quotient, conductor_eq_top_iff_adjoin_eq_top, Ideal.le_pow_of_le_ramificationIdx, MvPolynomial.eval₂_C_mk_eq_zero, Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne, Ideal.spanNorm_eq_bot_iff, NumberField.HeightOneSpectrum.one_lt_absNorm, Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf, Ideal.associatesEquivIsPrincipal_map_zero, Ideal.span_singleton_mul_right_injective, Ideal.Quotient.instNonemptyQuotient, MonomialOrder.sPolynomial_mem_ideal, MvPolynomial.mem_ideal_of_coeff_mem_ideal, Ideal.pow_lt_self, exists_multiset_prod_cons_le_and_prod_not_le, Ideal.absNorm_eq_zero_iff, Localization.le_comap_primeCompl_iff, PrimeSpectrum.zeroLocus_inf, isScalarTower_of_section_of_ker_sqZero, Finsupp.mem_ideal_span_range_iff_exists_finsupp, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, Module.supportDim_quotient_eq_ringKrullDim, PrimeSpectrum.mem_vanishingIdeal, Ideal.IsMaximal.lt_top, AdicCompletion.eval_of, FractionalIdeal.finite_factors', Valuation.mem_leIdeal_iff, PowerSeries.mem_hasEvalIdeal_iff, Ideal.span_univ, Submodule.IsMinimalPrimaryDecomposition.mem_image_radical_colon_iff, Submodule.torsionBySet_eq_torsionBySet_span, Ideal.exists_comap_eq_of_mem_minimalPrimes, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, Ideal.subset_union_prime, ringKrullDim_le_ringKrullDim_add_spanFinrank, Ideal.prod_eq_iInf_of_pairwise_isCoprime, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, idealFactorsFunOfQuotHom_coe_coe, IdealFilter.IsTorsionQuot.inf, Ideal.exists_ideal_over_prime_of_isIntegral, IsLinearTopology.hasBasis_ideal, Ideal.Quotient.finite_of_isInvariant, Ideal.exists_minimalPrimes_comap_eq, PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite, AdicCompletion.evalₐ_mk, DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ, not_dvd_differentIdeal_of_intTrace_not_mem, Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity, Ideal.KerLift.map_smul, IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_apply_mk, Algebra.QuasiFinite.finite_primesOver, RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one, Algebra.IsIntegral.quotient, count_associates_factors_eq, DoubleQuot.quotQuotEquivComm_mk_mk, Ideal.multiset_prod_le_inf, PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe, ValuationSubring.idealOfLE_top, Ideal.sInf_minimalPrimes, Ideal.torsionOf_eq_bot_iff_of_noZeroSMulDivisors, TwoSidedIdeal.orderIsoIsTwoSided_apply_coe, Submodule.coe_torsion_eq_annihilator_ne_bot, TwoSidedIdeal.asIdeal_matrix, Module.exists_surjective_quotient_of_finite, AlgHom.IsArithFrobAt.restrict_mk, FaithfulSMul.ker_algebraMap_eq_bot, AdicCompletion.evalₐ_mkₐ, AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_of_mem, Ideal.le_comap_sup, IsLocalization.coeSubmodule_strictMono, Ideal.Factors.isPrime, Ideal.ncard_primesOver_mul_card_inertia_mul_finrank, Irreducible.maximalIdeal_pow_eq_closedBall_pow, Algebra.Presentation.quotientEquiv_mk, PrimeSpectrum.primeSpectrumProd_symm_inl_asIdeal, conductor_eq_top_of_powerBasis, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, Polynomial.contentIdeal_le_span_content, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_inter, MvPolynomial.mem_vanishingIdeal_iff, WithIdealFilter.mem_nhds_iff, is_ideal_adic_pow, MvPolynomial.mem_vanishingIdeal_singleton_iff, Ideal.count_associates_eq', isSemiprimaryRing_iff, NumberField.RingOfIntegers.instNeZeroIdealOfIsMaximal, Ideal.pow_mem_pow, Ideal.ofList_cons, IsArtinianRing.primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal, Submodule.coe_mapAlgHom_apply, AlgHom.toKerIsLocalization_isLocalizedModule, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, Ideal.isPrimary_decomposition_pairwise_ne_radical, FractionalIdeal.equivNum_apply, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, IsTopologicallyNilpotent.mem_topologicalNilradical_iff, Ideal.homogeneousCore_eq_sSup, Ideal.iUnion_minimalPrimes, DividedPowers.isSubDPIdeal_inf_iff, ClassGroup.equiv_mk0, Ideal.ideal_prod_prime_aux, ContinuousMap.mem_idealOfSet_compl_singleton, Ideal.absNorm_bot, PrimeSpectrum.asIdeal_lt_asIdeal, Ideal.Quotient.quotient_ring_saturate, Ideal.comap_map_of_surjective', DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk, Ideal.relNorm_apply, Ideal.primesOver.isMaximal, RingHom.locally_iff_finite, Ideal.comap_fiberIsoOfBijectiveResidueField_symm, Ideal.Quotient.factorₐ_comp, Ideal.top_pow, AdicCompletion.val_zero, IsDedekindDomain.isOpen_of_ne_bot, Valuation.self_le_supp_comap, ProjectiveSpectrum.zeroLocus_span, isJacobsonRing_iff_sInf_maximal', NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, Ideal.mem_pi, Ideal.mk_ker, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, LinearMap.annihilator_le_of_surjective, MvPolynomial.mem_ideal_span_monomial_image, Ideal.mem_span_singleton_mul, Ideal.exists_spanRank_eq_and_height_eq, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, irreducible_pow_sup_of_le, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal, Ideal.height_le_height_add_spanFinrank_of_le, associatedPrimes.subset_union_of_exact, Ring.isField_iff_maximal_bot, Ideal.sup_pow_eq_top, Ideal.homogeneousCore_mono, Ideal.mul_top, Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing, DividedPowers.SubDPIdeal.lt_iff, Ideal.pow_eq_top_iff, AdicCompletion.mk_apply_coe, Submodule.torsionBySet.mk_smul, Ideal.IsPrime.prod_mem_iff_exists_mem, DualNumber.ideal_trichotomy, Ideal.Quotient.factor_comp, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply, Submodule.mem_annihilator_span_singleton, Algebra.TensorProduct.tensorQuotientEquiv_apply_tmul, sup_eq_prod_inf_factors, IsLocalRing.map_mkQ_eq_top, Algebra.idealMap_mul, RingHom.sub_mem_ker_iff, Ideal.inf_eq_mul_of_isCoprime, Derivation.liftKaehlerDifferential_apply, AlgebraicGeometry.Proj.localRingHom_comp_stalkIso_apply, Ideal.Quotient.mk_comp_algebraMap, Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree, Int.ideal_span_absNorm_eq_self, MonomialOrder.sPolynomial_mem_sup_ideal, KaehlerDifferential.DLinearMap_apply, Ideal.matrix_bot, DoubleQuot.coe_quotQuotEquivCommₐ, Ideal.mem_span_singleton, Ideal.radical_eq_top, Ideal.multiset_prod_eq_bot, Submodule.torsionBySet_ideal_isTorsion_of_noZeroDivisors, IsLocalization.mem_coeSubmodule, IsLocalRing.le_maximalIdeal_of_isPrime, HomogeneousIdeal.toIdeal_irrelevant_le, Ideal.mul_inf, RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last, RingTheory.Sequence.isWeaklyRegular_iff, Ideal.exists_disjoint_powers_of_span_eq_top, Ideal.relNorm_bot, Ideal.norm_mem_relNorm, StandardEtalePresentation.toPresentation_relation, Ideal.map_comap_le, Ideal.prod_span_singleton, Ideal.fst_comp_quotientInfEquivQuotientProd, Ideal.span_union, ClassGroup.mk0_eq_mk0_inv_iff, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf, Ideal.matrix_monotone, CharP.quotient_iff_le_ker_natCast, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_map_one, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, PrimeSpectrum.zeroLocus_sup, ProjectiveSpectrum.zeroLocus_iSup_ideal, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, IsDedekindDomain.exists_representative_mod_finset, Valuation.ltIdeal_mono, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι_ι, Ideal.mul_mem_left, Ideal.IsHomogeneous.sup, Polynomial.contentIdeal_mul_le_mul_contentIdeal, AdicCompletion.transitionMap_comp_eval_apply, Submodule.comap_smul'', ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap, IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk, Ideal.quotient_mk_maps_eq, TensorProduct.quotTensorEquivQuotSMul_comp_mk, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, isPRadical_iff, Ideal.IsHomogeneous.mul, IsLocalization.ideal_eq_iInf_comap_map_away, DoubleQuot.quotQuotEquivQuotOfLE_symm_mk, Localization.exists_awayMap_bijective_of_localRingHom_bijective, Ideal.spanNorm_mul_of_bot_or_top, WittVector.mem_span_p_iff_coeff_zero_eq_zero, Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton, Submodule.span_smul_span, isIntegral_quotientMap_iff, AdicCompletion.eval_lift_apply, Ideal.coeff_zero_mem_comap_of_root_mem, IsLocalization.mem_map_algebraMap_iff, Ideal.mul_mono_right, IsFractionRing.coeSubmodule_injective, AddValuation.comap_onQuot_eq, Ideal.mem_span_insert', PrimeSpectrum.localization_comap_range, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, RingHom.ker_eq, Ideal.IsMaximal.exists_inv_pow, NumberField.FinitePlace.norm_embedding', IsLocalization.orderIsoOfPrime_apply_coe, Ideal.IsHomogeneous.radical_eq, pNilradical_eq_bot_of_frobenius_inj, Polynomial.contentIdeal_le_contentIdeal_of_dvd, AlgebraicGeometry.Scheme.Hom.toImage_app, Ideal.ext_iff, Ideal.Quotient.lift_comp_mk, Algebra.HasGoingDown.exists_ideal_le_liesOver_of_lt, Algebra.isSeparable_residueField_iff, Ideal.absNorm_relNorm, AdicCompletion.val_zero_apply, Ring.le_comap_jacobson, Ideal.span_prod_le, HomogeneousIdeal.eq_top_iff, Ideal.mem_comap, RingHom.locally_iff_exists, Submodule.index_smul_le, Submodule.IsPrincipal.mem_iff_generator_dvd, SModEq.idealQuotientMk, exists_C_coeff_notMem, Int.absNorm_under_eq_sInf, Ideal.dvdNotUnit_iff_lt, Ideal.IsLocal.mem_jacobson_or_exists_inv, Ideal.algebraMap_residueField_eq_zero, Submodule.colon_iUnion, Ideal.absNorm_span_singleton, Ideal.radical_finset_inf, Algebra.FormallyEtale.iff_of_surjective, PreTilt.mk_untilt_eq_coeff_zero, PrimeSpectrum.range_comap_fst, FractionalIdeal.coeIdeal_absNorm, Ideal.Quotient.eq_factor_of_eq_factor_succ, Ideal.prod_sup_eq_top, FractionalIdeal.coeIdeal_injective', AlgHom.kerSquareLift_mk, Ideal.dvd_span_singleton, Ideal.Quotient.factor_eq, Ideal.nonPrincipals_eq_empty_iff, Ideal.bijective_algebraMap_quotient_residueField, Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul, Ideal.map_toCotangent_ker, Ideal.absNorm_algebraMap, PrimeSpectrum.zeroLocus_empty_iff_eq_top, Submodule.inf_colon, Ideal.isCoprime_iff_codisjoint, WittVector.mk_fontaineTheta, ProjectiveSpectrum.zeroLocus_inf, IdealFilter.isTorsionQuot_def, AlgebraicGeometry.StructureSheaf.comapₗ_eq_localRingHom, Ideal.map_pointwise_smul, Ideal.smul_mem_pointwise_smul_iff, DividedPowers.dpow_span_isSubideal, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, IsPRadical.ker_le', IsNilpotent.isUnit_quotient_mk_iff, Submodule.smul_top_le_comap_smul_top, Ideal.mem_sup_right, Submodule.set_smul_top_eq_span, Ideal.sup_mul, PrimeSpectrum.zeroLocus_anti_mono_ideal, IsAdicComplete.mk_comp_liftRingHom, Submodule.powSMulQuotInclusion_injective, Ideal.Quotient.norm_mk_le, Ideal.snd_comp_quotientInfEquivQuotientProd, Ideal.quotTorsionOfEquivSpanSingleton_apply_mk, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, Submodule.smul_le_span, Ring.exists_maximal_of_not_isField, Int.cast_mem_ideal_iff, Ideal.toIdeal_homogeneousCore_le, RingHom.surjectiveOnStalks_iff_forall_ideal, Ideal.isCoprime_iff_sup_eq, Ideal.IsPrime.radical_le_iff, Ideal.relNorm_map_algEquiv, Ideal.prime_of_isPrime, Algebra.SubmersivePresentation.basisCotangent_apply, Ideal.IsTwoSided.instHMul, Ideal.le_comap_mul, Ideal.mem_span_pow_iff_exists_isHomogeneous, Polynomial.annIdealGenerator_eq_zero_iff, emultiplicity_eq_emultiplicity_span, IsDedekindDomain.exists_sup_span_eq, PowerSeries.IsWeierstrassDivisorAt.seq_one, PrimeSpectrum.iSup_basicOpen_eq_top_iff', Algebra.kerTensorProductMapIdToAlgHomEquiv_symm_apply, DoubleQuot.quotLeftToQuotSupₐ_toRingHom, Ideal.hasFiniteMulSupport_inv, Ideal.span_pair_mul_span_pair, IsArtinianRing.isNilpotent_nilradical, Ideal.bot_quotient_isMaximal_iff, Ideal.toIdeal_homogeneousHull_eq_iSup, Ideal.exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem, Algebra.Extension.Cotangent.map_mk, Ideal.height_bot, Module.isTorsionBy_iff_mem_annihilator, IsArtinianRing.isSemisimpleRing_iff_jacobson, AdicCompletion.eval_surjective, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, AdicCompletion.ofPowSMul_val_apply, cardQuot_mul_of_coprime, isAdic_iff, IsLocalization.comap_le_comap_iff, Submodule.FG.smul, Ideal.coe_smul_primesOver, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, Module.associatedPrimes.comap_mem_associatedPrimes_of_mem_associatedPrimes_of_isLocalizedModule_of_fg, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal', AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_iff, MixedCharZero.reduce_to_maximal_ideal, Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver, Ideal.homogeneousHull_eq_sInf, IsLocalization.coeSubmodule_top, Ideal.span_singleton_absNorm_le, Ideal.bot_liesOver_bot, Ideal.exists_map_eq_of_isGalois, Ideal.isCoprime_of_isMaximal, Ideal.Factors.piQuotientEquiv_mk, Ideal.eq_top_of_mk_tensor_eq_one, conductor_eq_top_of_adjoin_eq_top, Ideal.sup_mul_left_self, Ideal.IsMaximal.exists_inv, Ideal.quotient_map_mkₐ, RingHom.kerLift_mk, Ideal.finprod_not_dvd, Ideal.natAbs_det_basis_change, Perfection.teichmuller₀_mapMonoidHom_idealQuotientMk, PadicInt.coe_dpow_eq, Ideal.bot_prime, Module.mem_support_iff_of_span_eq_top, Ideal.instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia, IsLocalRing.finite_quotient_iff, Ideal.leadingCoeffNth_mono, QuotientRing.isOpenQuotientMap_mk, KaehlerDifferential.fromIdeal_surjective, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, Ideal.quotientEquivAlgOfEq_symm, AdicCompletion.transitionMap_map_one, AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal, Polynomial.IsEisensteinAt.leading, RingHom.surjectiveOnStalks_iff_forall_maximal, IsLocalization.map_algebraMap_ne_top_iff_disjoint, QuotSMulTop.mem_annihilator, Ideal.mem_of_localization_maximal, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, Ideal.Quotient.isScalarTower_right, pow_sub_one_dvd_differentIdeal_aux, Ideal.mul_right_self_sup, Ideal.spanNorm_top, ClassGroup.integralRep_mem_nonZeroDivisors, IsLocalRing.local_hom_TFAE, Ideal.one_notMem, HenselianRing.jac, LinearMap.ker_tensorProductMk, Ideal.ringChar_quot, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Ideal.mem_iSup_of_mem, Ideal.toCotangent_surjective, FractionalIdeal.num_eq_zero_iff, Ideal.coe_piOrderIso_apply, Ideal.cotangentIdeal_square, Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul, IsDedekindDomain.HeightOneSpectrum.associates_irreducible, CharP.quotient_iff, Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson, Ideal.mul_sub_mul_mem, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, Ideal.eval₂_C_mk_eq_zero, Ideal.IsHomogeneous.iSup₂, Polynomial.IsWeaklyEisensteinAt.mem, pNilradical_eq_bot', AddValuation.supp_quot_supp, Polynomial.coeff_mem_contentIdeal, Ideal.finite_quotient_prod, Ideal.Quotient.liftₐ_comp, Ideal.Quotient.mk_smul_mk_quotient_map_quotient, Ideal.mem_span_singleton_self, AdicCompletion.eval_apply, Ideal.mul_eq_bot, Ideal.map_pow, RingHom.toKerIsLocalization_isLocalizedModule, PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain, Algebra.idealMap_apply_coe, Int.liesOver_span_absNorm, Ideal.map_eq_top_of_bijective, IsLocalization.coeSubmodule_sup, AlgebraicGeometry.localRingHom_comp_stalkIso, AddValuation.supp_quot, PrimeSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal, HomogeneousIdeal.toIdeal_inf, IsLocalRing.isOpen_iff_finite_quotient, Nat.one_mem_span_iff, Ideal.Quotient.mkₐ_surjective, PrimeSpectrum.vanishingIdeal_iUnion, injective_lTensor_quotient_iff_inf_eq_mul, PrimeSpectrum.isCompact_isOpen_iff_ideal, AlgebraicGeometry.Proj.localRingHom_comp_stalkIso, Ideal.finite_mulSupport_inv, IsDedekindDomain.quotientEquivPiFactors_mk, IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_eq_one_iff, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso, pNilradical_le_nilradical, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, Submodule.annihilator_eq_top_iff, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, IsArithFrobAt.conj, Ring.jacobson_lt_top, Ring.jacobson_quotient_jacobson, Submodule.disjoint_torsionBySet_ideal, Ideal.primaryComponent_torsionBySet_of_isCoprime, Algebra.FinitePresentation.quotient, Ideal.map_iSup, AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq, Ideal.comap_injective_of_surjective, NumberField.FinitePlace.norm_embedding_int, Module.IsTorsionBy.mk_smul, instCompactSpaceQuotientIdeal, Ring.jacobson_eq_sInf_isMaximal, RingTheory.Sequence.isRegular_cons_iff', HomogeneousIdeal.toIdeal_iSup, Module.annihilator_le_of_mem_support, Ideal.IsHomogeneous.iInf₂, FractionalIdeal.coe_mk0, Submodule.colon_bot, TrivSqZeroExt.mem_kerIdeal_iff_inr, PrimeSpectrum.zeroLocus_pow, IsLocalization.AtPrime.map_eq_top_of_not_le, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, Ideal.associatesEquivIsPrincipal_map_one, Algebra.Generators.ker_naive, Polynomial.exists_monic_aeval_eq_zero_forall_mem_of_mem_map, Ideal.span_insert, Ideal.Quotient.zero_eq_one_iff, PrimeSpectrum.vanishingIdeal_mem_minimalPrimes, Ideal.Fiber.exists_smul_eq_one_tmul, Ideal.finiteQuotientOfFreeOfNeBot, IsFractionRing.ideal_span_singleton_map_subset, AlgebraicGeometry.Scheme.Hom.liftQuotient_comp_assoc, Ideal.mapHom_apply, Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, Ideal.hasBasis_nhds_adic, Ideal.relNorm_eq_pow_of_isMaximal, DoubleQuot.coe_liftSupQuotQuotMkₐ, IsDedekindDomain.HeightOneSpectrum.ideal_ne_top_iff_exists, Algebra.Extension.Cotangent.ker_mk, Submodule.IsPrimary.mem_or_mem, AdicCompletion.val_sum_apply, AlgebraicGeometry.Scheme.localRingHom_comp_stalkIso_apply, Ideal.pointwise_smul_toAddSubmonoid, AdicCompletion.evalOneₐ_liftAlgHom, singleton_span_mem_normalizedFactors_of_mem_normalizedFactors, IsLocalRing.map_maximalIdeal_lt_top, IsLocalization.coe_primeSpectrumOrderIso_apply_coe_asIdeal, Ideal.primaryComponent_torsionBySet_eq_inf, Ideal.span_singleton_pow, Polynomial.IsEisensteinAt.notMem, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Ideal.comap_lt_comap_of_root_mem_sdiff, Ideal.le_jacobson, HomogeneousIdeal.mem_iff, RingPreordering.support_eq_bot, PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk, Ideal.gc_map_comap, AdicCompletion.evalₐ_liftRingHom, Int.instFiniteQuotientIdealSpanSingletonSetOfNeZero, IsAdicComplete.StrictMono.mkQ_comp_lift, PrimeSpectrum.le_vanishingIdeal_zeroLocus, map_prime_of_equiv, Perfection.teichmuller_spec, Nat.absNorm_under_prime, Perfection.teichmullerAux_sModEq, PadicInt.existsUnique_mem_range, Ideal.Quotient.maximal_ideal_iff_isField_quotient, Algebra.FormallyEtale.comp_bijective, Int.quotientSpanNatEquivZMod_comp_castRingHom, Nat.coe_maximalIdeal, IsDedekindDomain.HeightOneSpectrum.adicAbv_coe_lt_one_iff, Submodule.torsionBy.mk_smul, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, Polynomial.IsEisensteinAt.coeff_mem, Ideal.finprod_heightOneSpectrum_factorization, IsLocalization.coeSubmodule_injective, PadicInt.toZMod_spec, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, FractionalIdeal.coeIdeal_pow, IsLocalRing.spanFinrank_eq_finrank_quotient, instFiniteQuotientIdealOfIsMaximal, FractionalIdeal.count_coe, Ideal.mem_inv_pointwise_smul_iff, TwoSidedIdeal.coe_asIdeal, UniformSpace.inseparableSetoid_ring, Ideal.radical_mul, Ideal.IsPrime.mul_mem_iff_mem_or_mem, MvPolynomial.mem_ideal_span_X_image, AdicCompletion.of_apply, Ideal.pointwise_smul_def, WittVector.ghostComponentModPPow_map_mk, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem, Algebra.FormallySmooth.iff_comp_surjective, Polynomial.IsDistinguishedAt.coe_natDegree_eq_order_map, ContinuousMap.idealOpensGI_choice, Ideal.comap_jacobson, IsDedekindDomain.isOpen_iff, NumberField.FinitePlace.norm_def, IsAdicComplete.StrictMono.mk_lift, Ideal.kerLiftAlg_mk, Ideal.relNorm_comap_algEquiv, MvPolynomial.mem_image_comap_C_basicOpen, IsLocalRing.isOpen_maximalIdeal, Algebra.Presentation.mem_ker_naive, Perfection.teichmuller_spec', Ideal.isRadical_iff_quotient_reduced, AlgebraicGeometry.Scheme.IdealSheafData.le_def, AlgHom.IsArithFrobAt.restrict_apply, Ideal.pi_quotient_surjective, Ideal.instIsCoatomic, Ideal.IsOka.top, DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk, Ideal.comap_le_iff_le_map, Ideal.mem_prod, Ideal.exists_pow_inf_eq_pow_smul, Algebra.Extension.cotangentComplex_mk, AlgHom.IsArithFrobAt.finite_quotient, RingHom.surjective_localRingHom_iff, CompleteOrthogonalIdempotents.bijective_pi, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal, IdealFilter.isUniform_iff_exists_ringFilterBasis, AdicCompletion.eval_comp_of, Ideal.to_quotient_square_comp_toCotangent, ringKrullDim_le_ringKrullDim_quotient_add_encard, retractionOfSectionOfKerSqZero_tmul_D, Ideal.IsHomogeneous.mem_iff, Ideal.map_eq_bot_iff_le_ker, AdicCompletion.val_smul_apply, Module.annihilator_prod, Ideal.le_comap_pow_ramificationIdx, DoubleQuot.quotQuotEquivComm_symm, Ideal.mem_jacobson_bot, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, Ideal.span_iUnion, IsCoprime.codisjoint, Ideal.Factors.piQuotientEquiv_map, AlgebraicGeometry.Scheme.IdealSheafData.supportSet_eq_iInter_zeroLocus, instIsFractionRingQuotientIdealResidueField, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, Ideal.sup_multiset_prod_eq_top, Ideal.span_range_eq_iSup, IsLocalRing.primesOver_eq, Ideal.stabilizerEquiv_apply_smul, mem_nilradical, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, derivationQuotKerSq_mk, Ideal.isoBaseOfIsPrincipal_apply, Submodule.map_le_smul_top, Ideal.homogeneousCore.gc, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, IsCoprime.add_eq, Algebra.Generators.C_mul_X_sub_one_mem_ker, Ideal.eq_bot_of_liesOver_bot, Ideal.Quotient.noZeroDivisors, Ideal.mem_minimalPrimes_of_krullDimLE_zero, FractionalIdeal.coeIdeal_finprod, Ideal.eq_zero_of_polynomial_mem_map_range, Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul, Ideal.isOpen_of_isMaximal, Ideal.span_singleton_mul_le_iff, PrimeSpectrum.range_asIdeal, Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff, DoubleQuot.quotQuotEquivComm_algebraMap, Submodule.exists_sub_one_mem_and_smul_le_of_fg_of_le_sup, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, Ideal.le_colon, Submodule.spanRank_bot, Ideal.Quotient.mk_algebraMap, FractionalIdeal.coeIdeal_le_coeIdeal, AdicCompletion.eval_lift, Ideal.absNorm_dvd_norm_of_mem, Perfection.teichmullerFun_eq_teichmuller₀, Algebra.FormallyUnramified.iff_comp_injective_of_small, Ideal.Cotangent.lift_surjective_iff, PrimeSpectrum.asIdeal_le_asIdeal, IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod, Polynomial.isIntegral_isLocalization_polynomial_quotient, Ideal.Quotient.algebraMap_mk_of_liesOver, IsArtinianRing.setOf_isMaximal_finite, PrimeSpectrum.zeroLocus_eq_singleton, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span, RingQuot.ringQuotToIdealQuotient_apply, IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing, Module.notMem_support_iff', Ideal.isMaximal_def, Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective, PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply, Ideal.cotangent_subsingleton_iff, Ideal.mulQuot_injective, AlgebraicGeometry.IsAffineOpen.mem_ideal_iff
topologicalRingQuotientTopology 📖	CompOp	5 math math: QuotientRing.isOpenMap_coe, QuotientRing.isQuotientMap_coe_coe, topologicalRing_quotient, QuotientRing.isOpenQuotientMap_mk, instCompactSpaceQuotientIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCompactSpaceQuotientIdeal 📖	mathematical	—	CompactSpace HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 topologicalRingQuotientTopology	—	Quotient.compactSpace
topologicalRing_quotient 📖	mathematical	—	IsTopologicalRing HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 topologicalRingQuotientTopology NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing	—	AddSubgroup.normal_of_comm QuotientAddGroup.instIsTopologicalAddGroup IsSemitopologicalRing.toIsTopologicalAddGroup IsTopologicalRing.toIsSemitopologicalRing IsTopologicalAddGroup.toContinuousAdd Ideal.instIsTwoSided_1 Topology.IsQuotientMap.continuous_iff QuotientRing.isQuotientMap_coe_coe Continuous.comp continuous_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalAddGroup.toContinuousNeg

---

← Back to Index