span π | CompOp | 529 mathmath: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', span_pair_left_add, IsAdjoinRoot.repr_add_sub_repr_add_repr_mem_span, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, RingHom.ker_evalRingHom, MonomialOrder.span_leadingTerm_sdiff_singleton_zero, span_le, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow, Algebra.Extension.Cotangent.span_eq_top_of_span_eq_ker, span_pair_eq_span_right_iff_dvd, pow_multiset_sum_mem_span_pow, PadicInt.lift_sub_val_mem_span, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, Int.quotientSpanEquivZMod_comp_Quotient_mk, Polynomial.ker_evalRingHom, Polynomial.Monic.free_quotient, StandardEtalePair.inv_aeval_X_g, span_singleton_mul_le_span_singleton_mul, mem_span_iff_exists_isHomogeneous, ClassGroup.mk0_eq_mk0_iff, Algebra.Presentation.naive_toGenerators, subset_span, absNorm_span_insert, RingTheory.Sequence.isWeaklyRegular_cons_iff', squarefree_span_singleton, mem_span_singleton', IsHomogeneous.iff_exists, ClassGroup.mk_eq_mk_of_coe_ideal, Algebra.PreSubmersivePresentation.ofHasCoeffs_map, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, FractionalIdeal.coeIdeal_span_singleton, exists_mem_span_singleton_map_residueField_eq, PreTilt.valAux_eq, IsLocalization.coeSubmodule_span, finrank_quotient_span_eq_natDegree_norm, span_singleton_dvd_span_singleton_iff_dvd, le_span_singleton_mul_iff, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, Polynomial.idealX_span, span_prod, PadicInt.appr_spec, mem_colon_span_singleton, smul_closure, ringKrullDim_eq_one_iff_of_isLocalRing_isDomain, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, Polynomial.quotientSpanXSubCAlgEquiv_symm_apply, span_singleton_eq_span_singleton, QuotSMulTop.equivTensorQuot_naturality, span_pow_eq_map_homogeneousSubmodule, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_mk, span_singleton_mul_right_unit, span_singleton_mul_left_injective, Int.quotientSpanNatEquivZMod_comp_Quotient_mk, Submodule.ideal_span_singleton_smul, StandardEtalePresentation.toPresentation_algebra_smul, span_eq_map_homogeneousSubmodule, span_pair_add_left, exists_finset_card_eq_height_of_isNoetherianRing, PowerSeries.maximalIdeal_eq_span_X, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, WittVector.factorPowSucc_comp_fontaineThetaModPPow, PowerBasis.quotientEquivQuotientMinpolyMap_apply, PreTilt.coeff_pow_p, FractionalIdeal.count_well_defined, associatesNonZeroDivisorsEquivIsPrincipal_apply, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, span_singleton_eq_bot, IsLocalization.mem_span_map, submodule_span_eq, span_pow_eq_top, finrank_quotient_span_eq_natDegree', map_spanIntNorm, AlgEquiv.prodQuotientOfIsIdempotentElem_apply, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', instIsPrincipalSpanSingletonSet, Polynomial.contentIdeal_def, Nat.exists_mem_span_nat_finset_of_ge, WittVector.factorPowSucc_fontaineThetaModPPow_eq, QuotSMulTop.equivTensorQuot_naturality_mk, DividedPowers.SubDPIdeal.dpow_mem_span_of_mem_span, span_pair_add_left_mul, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal, absNorm_eq_pow_inertiaDeg', span_pair_right_add, range_mul', Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, IsDedekindDomain.exists_eq_span_pair, PadicInt.maximalIdeal_eq_span_p, PrimeSpectrum.union_zeroLocus, AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, AdjoinRoot.evalEval_apply, span_gcd, prime_span_singleton_iff, sup_eq_top_iff_isCoprime, span_pair_sub_left', factors_decreasing, span_le_of_C_coeff_mem, PrimeSpectrum.iSup_basicOpen_eq_top_iff, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow, Polynomial.span_singleton_annIdealGenerator, isPrime_int_iff, span_pair_comm, PreTilt.mk_comp_untilt_eq_coeff_zero, Algebra.PreSubmersivePresentation.ofHasCoeffs_Ο', span_pair_sub_mul_right, WittVector.mk_pow_fontaineTheta, Submodule.IsPrincipal.contentIdeal_le_span_iff_dvd, PreTilt.coeff_frobeniusEquiv_symm, AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHom, iSup_eq_span, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime, RingHom.locally_iff_isLocalization, PrimeSpectrum.zeroLocus_span, range_mul, span_singleton_abs, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, Nat.subset_span_setGcd, CharP.ker_intAlgebraMap_eq_span, finrank_quotient_eq_sum, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, Int.card_ideal_quot, span_pair_right_mul_add, relNorm_singleton, map_relNorm, Polynomial.mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, Algebra.Presentation.naive_relation, span_singleton_mul_eq_span_singleton_mul, eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne, ProjectiveSpectrum.union_zeroLocus, Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero, span_singleton_one, FractionalIdeal.finprod_heightOneSpectrum_factorization, span_eq_top_iff_finite, Submodule.coe_span_smul, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, span_single_eq_top, IsIdempotentElem.ker_toSpanSingleton_eq_span, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, span_pair_zero, MonomialOrder.span_leadingTerm_eq_span_monomial, IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd, MonomialOrder.span_leadingTerm_eq_span_monomialβ, span_singleton_le_span_singleton, DualNumber.maximalIdeal_eq_span_singleton_eps, mem_span_range_self, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, FractionalIdeal.count_ne_zero, span_singleton_mul_right_inj, height_le_height_add_one_of_mem, finrank_quotient_span_eq_natDegree, ModP.preVal_mul, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, iInf_span_singleton_natCast, MvPolynomial.pow_idealOfVars_eq_span, AddMonoidAlgebra.mem_ideal_span_of'_image, Int.span_natAbs, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, DualNumber.isMaximal_span_singleton_eps, span_sdiff_singleton_zero, WittVector.mem_span_p_pow_iff_le_coeff_eq_zero, Nat.finite_setOf_setGcd_dvd_and_mem_span, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow, span_singleton_zero, multiset_prod_span_singleton, Quotient.eq_zero_iff_dvd, Polynomial.idealSpan_range_update_divByMonic, map_span, Polynomial.ker_constantCoeff, Int.ideal_span_isMaximal_of_prime, span_singleton_generator, span_pair_add_right_mul, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, Quotient.mk_singleton_self, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, torsionOf_eq_span_pow_pOrder, eq_span_singleton_mul, Algebra.Presentation.naive_relation_apply, Associates.le_singleton_iff, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, AdjoinRoot.span_maximal_of_irreducible, AdjoinRoot.quotEquivQuotMap_apply, AlgebraicGeometry.IsAffineOpen.self_le_basicOpen_union_iff, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, IsSemisimpleRing.ideal_eq_span_idempotent, CharacterModule.intSpanEquivQuotAddOrderOf_apply, PowerBasis.exists_smodEq, PrimeSpectrum.zeroLocus_subset_zeroLocus_singleton_iff, Valuation.pow_Uniformizer_is_pow_generator, mem_span_C_coeff, IsPrimitiveRoot.finite_quotient_span_sub_one', AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, IsDiscreteValuationRing.irreducible_iff_uniformizer, IsPrimitiveRoot.finite_quotient_span_sub_one, Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors, PreTilt.coeff_frobenius, Quotient.mk_span_range, Algebra.PreSubmersivePresentation.naive_toPresentation, Polynomial.quotientSpanXSubCAlgEquiv_mk, isFiniteLength_quotient_span_singleton, AlgebraicGeometry.isOpenImmersion_SpecMap_iff_of_surjective, FractionalIdeal.coe_ideal_span_singleton_div_self, NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm, RingOfIntegers.not_dvd_exponent_iff, ringKrullDim_le_ringKrullDim_quotient_add_card, MonomialOrder.span_leadingTerm_eq_span_monomial', exact_mulQuot_quotOfMul, span_singleton_nonZeroDivisors, span_singleton_eq_top, PreTilt.coeff_iterate_frobeniusEquiv_symm, height_le_ringKrullDim_quotient_add_one, Algebra.Presentation.span_range_relation_eq_ker, IsIdempotentElem.ker_toSpanSingleton_one_sub_eq_span, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, span_mul_span', homogeneousHull_eq_iSup, span_pair_sub_left_mul, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_symm_mk, RingHom.pi_bijective_of_isIdempotentElem, QuotSMulTop.equivQuotTensor_naturality, ModP.preVal_mk, Int.quotientSpanEquivZMod_comp_castRingHom, relNorm_int, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, dvd_generator_iff, isRadical_iff_span_singleton, IsCyclotomicExtension.Rat.inertiaDeg_eq, IsLocalization.Away.span_range_mulNumerator_eq_top, mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert, NumberField.HeightOneSpectrum.embedding_mul_absNorm, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipal, WittVector.ker_map_le_ker_mk_comp_ghostComponent, span_eq, count_span_normalizedFactors_eq_of_normUnit, IsAdjoinRoot.repr_zero_mem_span, IsLocalization.Away.quotient_of_isIdempotentElem, span_singleton_le_iff_mem, span_pair_sub_mul_left, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, WittVector.fontaineThetaModPPow_teichmuller, IsBezout.iff_span_pair_isPrincipal, Algebra.Generators.ker_localizationAway, mem_span_singleton_sup, finset_inf_span_singleton, OrthogonalIdempotents.surjective_pi, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', span_mul_span, span_one, basisSpanSingleton_apply, Submodule.torsionBySet_ideal_span_singleton_eq, Algebra.Generators.comp_localizationAway_ker, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff, WittVector.ghostComponentModPPow_teichmuller_coeff, Algebra.Smooth.exists_span_eq_top_isStandardSmooth, height_le_ringKrullDim_quotient_add_encard, RingHom.prod_bijective_of_isIdempotentElem, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one', IsCyclotomicExtension.Rat.ncard_primesOver_of_prime, IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one, iInf_span_singleton, Module.isTorsionBySet_iff_is_torsion_by_span, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors, AdjoinRoot.quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, WittVector.isAdicCompleteIdealSpanP, Submodule.torsionBy.mk_ideal_smul, Polynomial.contentIdeal_C, span_pair_add_mul_left, IsDiscreteValuationRing.ideal_eq_span_pow_irreducible, pi_span, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, span_singleton_mul_span_singleton, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, Polynomial.Monic.finite_quotient, span_pair_abs, Valued.integer.coe_span_singleton_eq_closedBall, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson, PadicInt.mem_span_pow_iff_le_valuation, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, quotOfMul_surjective, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, span_singleton_toAddSubgroup_eq_zmultiples, span_insert_neg, span_pair_eq_span_left_iff_dvd, Ring.DirectLimit.quotientMk_of, Rat.HeightOneSpectrum.span_natGenerator, exists_subset_radical_span_sup_of_subset_radical_sup, PadicInt.norm_le_pow_iff_mem_span_pow, sum_pow_mem_span_pow, Int.ringChar_idealQuot, associated_norm_prod_smith, MvPolynomial.ker_evalβHom_universalFactorizationMap, constr_basisSpanSingleton, PadicInt.ker_toZModPow, Polynomial.contentIdeal_monomial, span_singleton_mul_left_mono, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, ringKrullDim_le_ringKrullDim_add_card, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, IsDedekindDomain.HeightOneSpectrum.intValuation_def, mem_span, mem_span_range_iff_exists_fun, QuotSMulTop.equivQuotTensor_naturality_mk, isPrime_nat_iff, associatesEquivIsPrincipal_apply, HomogeneousIdeal.irrelevant_eq_span, MonomialOrder.span_leadingTerm_insert_zero, span_range_pow_eq_top, DividedPowers.span_isSubDPIdeal_iff, Submodule.IsPrincipal.dvd_generator_span_iff, PowerSeries.exist_eq_span_eq_ncard_of_X_notMem, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd, span_singleton_mul_right_mono, Polynomial.span_minpoly_eq_annihilator, Polynomial.coeff_mem_radical_span_coeff_of_dvd, MonoidAlgebra.mem_ideal_span_of_image, FractionalIdeal.coe_ideal_span_singleton_inv_mul, Valuation.Integers.coe_span_singleton_eq_setOf_le_v_algebraMap, IsPrimitiveRoot.card_quotient_toInteger_sub_one, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, ZMod.ker_intCastRingHom, isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors, IsCyclotomicExtension.Rat.inertiaDegIn_eq, StandardEtalePresentation.toPresentation_Ο', FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal, count_associates_eq, Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite, Irreducible.maximalIdeal_eq, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, span_pair_sub_left, WittVector.quotientPEquiv_mk, AlgEquiv.prodQuotientOfIsIdempotentElem_apply_snd, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, ModP.preVal_zero, spanNorm_singleton, count_span_normalizedFactors_eq, span_pair_add_mul_right, span_singleton_inf_span_singleton, span_singleton_mem_isPrincipalSubmonoid, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, span_eq_bot, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk, span_zero, factors_span_eq, ModP.instCharPOfPrimeOfFactNotIsUnitCast, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, Nat.span_singleton_setGcd, prod_span, MvPolynomial.zeroLocus_span, span_singleton_mul_left_unit, PreTilt.coeff_iterate_frobenius, StandardEtalePair.aeval_X_g_mul_mk_X, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_pow_mul_prod, span_pair_left_mul_add, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk, span_mono, Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, AlgEquiv.prodQuotientOfIsIdempotentElem_apply_fst, AlgebraicGeometry.Scheme.zeroLocus_span, homogeneous_span, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, isPrime_iff_of_isPrincipalIdealRing, colon_span, DividedPowers.SubDPIdeal.span_carrier_eq_dpow_span, span_pair_sub_right_mul, Submodule.IsPrincipal.associated_generator_span_self, IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd, CharP.quotient, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, mem_span_pair, span_empty, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, span_singleton_mul_left_inj, span_insert_zero, span_singleton_lt_span_singleton, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd, span_singleton_absNorm, span_pair_mul_left_add, PrimeSpectrum.basicOpen_le_basicOpen_iff, KaehlerDifferential.span_range_eq_ideal, mem_mul_span_singleton, isCoprime_span_singleton_iff, WittVector.quotEquivOfEq_ghostComponentModPPow, AdjoinRoot.quotEquivQuotMap_symm_apply, CompleteOrthogonalIdempotents.bijective_pi', NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, StandardEtalePresentation.toPresentation_val, height_le_height_add_encard_of_subset, conductor_mul_differentIdeal, Nat.maximalIdeal_eq_span_two_three, MvPolynomial.mem_ideal_span_monomial_image_iff_dvd, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, absNorm_eq_pow_inertiaDeg, Submodule.finrank_quotient_eq_sum, span_pair_sub_right, mem_span_insert, ClassGroup.mk_eq_one_of_coe_ideal, Submodule.span_smul_eq, IsCyclotomicExtension.Rat.ramificationIdx_eq, Valuation.IsUniformizer.is_generator, AlgebraicGeometry.IsAffineOpen.basicOpen_union_eq_self_iff, span_singleton_mul_right_injective, Finsupp.mem_ideal_span_range_iff_exists_finsupp, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, FractionalIdeal.finite_factors', span_univ, Submodule.torsionBySet_eq_torsionBySet_span, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, span_singleton_prime, span_range_eq_span_range_support, PowerSeries.span_X_isPrime, ofList_singleton, span_pair_add_right, RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one, span_pair_mul_right_add, PadicInt.ideal_eq_span_pow_p, CharacterModule.intSpanEquivQuotAddOrderOf_apply_self, Polynomial.contentIdeal_le_span_content, count_associates_eq', EuclideanDomain.span_gcd, ofList_cons, FractionalIdeal.coe_ideal_span_singleton_mul_inv, Valuation.Uniformizer.is_generator, IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd, relNorm_apply, RingHom.locally_iff_finite, ProjectiveSpectrum.zeroLocus_span, WittVector.ker_constantCoeff, MvPolynomial.mem_ideal_span_monomial_image, mem_span_singleton_mul, DualNumber.ideal_trichotomy, Int.ideal_span_absNorm_eq_self, mem_span_singleton, ModP.preVal_add, StandardEtalePresentation.toPresentation_relation, prod_span_singleton, span_union, ClassGroup.mk0_eq_mk0_inv_iff, IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, PrimeSpectrum.mem_image_comap_zeroLocus_sdiff, ModP.preVal_eq_zero, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, WittVector.mem_span_p_iff_coeff_zero_eq_zero, Submodule.span_smul_span, mem_span_insert', FirstOrder.Ring.mvPolynomial_zeroLocus_definable, span_prod_le, RingHom.locally_iff_exists, absNorm_span_singleton, PreTilt.mk_untilt_eq_coeff_zero, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd, IsBezout.span_gcd_eq_span_gcd, dvd_span_singleton, WittVector.mk_fontaineTheta, DividedPowers.dpow_span_isSubideal, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, Submodule.set_smul_top_eq_span, Submodule.smul_le_span, IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime, mem_span_pow_iff_exists_isHomogeneous, emultiplicity_eq_emultiplicity_span, IsDedekindDomain.exists_sup_span_eq, PrimeSpectrum.iSup_basicOpen_eq_top_iff', span_pair_mul_span_pair, toIdeal_homogeneousHull_eq_iSup, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime, span_insert_abs, Polynomial.ker_modByMonicHom, span_singleton_absNorm_le, PadicInt.coe_dpow_eq, Module.Basis.SmithNormalForm.toAddSubgroup_index_eq_ite, IsBezout.span_gcd, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, minpoly.ker_eval, mem_span_singleton_self, Int.liesOver_span_absNorm, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime, Nat.one_mem_span_iff, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, span_pair_neg, Module.IsTorsionBy.mk_smul, RingTheory.Sequence.isRegular_cons_iff', IsBezout.span_pair_isPrincipal, span_insert, IsFractionRing.ideal_span_singleton_map_subset, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, singleton_span_mem_normalizedFactors_of_mem_normalizedFactors, span_singleton_pow, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, PreTilt.coeff_def, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, Int.instFiniteQuotientIdealSpanSingletonSetOfNeZero, IsAdjoinRoot.ker_map, Int.quotientSpanNatEquivZMod_comp_castRingHom, MvPolynomial.mem_ideal_span_X_image, WittVector.ghostComponentModPPow_map_mk, PreTilt.coeff_iterate_frobenius', Algebra.Presentation.mem_ker_naive, CompleteOrthogonalIdempotents.bijective_pi, span_singleton_neg, ringKrullDim_le_ringKrullDim_quotient_add_encard, span_iUnion, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, span_range_eq_iSup, span_pair_sub_right', span_singleton_mul_le_iff, PowerSeries.eq_span_insert_X_of_X_mem_of_span_eq, KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span, IsLocalization.coeSubmodule_span_singleton, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply
|