instPreorder 📖 | CompOp | 1543 mathmath: SchwartzMap.norm_toLp_le_seminorm, Behrend.roth_lower_bound, CuspFormClass.qExpansion_isBigO, Polynomial.degree_map_le, isEquivalent_descFactorial, LTSeries.head_add_length_le_nat, Polynomial.modByMonic_eq_self_iff, NNReal.tendsto_agmSequences_fst_agm, Set.ncard_mono, List.sorted_lt_range, Set.IsPWO.exists_monotone_subseq, Measurable.limsup, IsAlgClosed.roots_eq_zero_iff_degree_nonpos, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two', mapClusterPt_atTop_pow_tfae, Finset.sum_Ico_sub_bot, MvPowerSeries.WithPiTopology.tendsto_trunc_atTop, ProbabilityTheory.Kernel.tendsto_m_density, seminormFromConst_seq_antitone, AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound, Finset.sum_Ico_Ico_comm', Polynomial.degree_mul_le, NormedAddCommGroup.cauchy_series_of_le_geometric'', pow_self_strictMonoOn, rothNumberNat_spec, LightProfinite.proj_comp_transitionMap, Polynomial.exists_degree_le_of_mem_span_of_finite, Filter.limsup_nat_add, LightProfinite.Extend.functorOp_obj, LinearMap.iterateRange_succ, StrictMono.strictAnti_iterate_of_map_lt, FormalMultilinearSeries.comp_partialSum, tendsto_birkhoffAverage_apply_sub_birkhoffAverage', MvPowerSeries.eq_iff_frequently_trunc'_eq, ProbabilityTheory.measure_limsup_eq_one, Fin.preimage_val_Ici_val, ExpGrowth.eventually_le_exp, tendsto_smoothingFun_of_ne_zero, HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn, exists_strictMono, Finset.sum_Ico_eq_add_neg, tendsto_tsum_div_pow_atTop_integral, RCLike.tendsto_inverse_atTop_nhds_zero_nat, Polynomial.Sequence.basis_natDegree_strictMono, hasSum_iff_tendsto_nat_of_summable_norm, PNat.map_subtype_embedding_Ico, Order.sequenceOfCofinals.monotone, exists_strictAnti', Finset.card_strictMono, Fin.isAddFreimanIso_Iio, GenContFract.of_convergence, primeFactorsList_sorted, Finsupp.toMultiset_strictMono, MeasureTheory.liminf_ae_eq_of_forall_ae_eq, tendsto_const_div_atTop_nhds_zero_nat, Polynomial.coe_lt_degree, Stirling.factorial_isEquivalent_stirling, galoisConnection_mul_div, Polynomial.degree_le_degree, Fin.image_val_Iic, Ioc_filter_modEq_cast, FirstOrder.Language.BoundedFormula.castLE_castLE, Fin.attachFin_Iic, exists_strictMono', succPNat_mono, Ioc_succ_singleton, ProbabilityTheory.Kernel.partialTraj_succ_of_le, MeasureTheory.eventually_mem_spanningSets, MeasureTheory.TendstoInMeasure.exists_seq_tendstoInMeasure_atTop, Complex.GammaSeq_tendsto_Gamma, MeasureTheory.preimage_spanningSetsIndex_singleton, exists_monotone_Icc_subset_open_cover_Icc, MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae, NormedAddCommGroup.cauchy_series_of_le_geometric', ack_strictMono_left, SSet.ofSimplex_le_skeleton, Cubic.degree_of_b_eq_zero, Polynomial.degree_quadratic_lt, Ico_succ_left_eq_erase_Ico, IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow, largeSchroder_succ, PNat.Icc_eq_finset_subtype, CompleteLatticeHom.apply_limsup_iterate, one_div_pow_strictAnti, WellFoundedGT.monotone_chain_condition, Finset.sum_range_add_sum_Ico, image_Ico_mod, AkraBazziRecurrence.exists_eventually_const_mul_le_r, tendsto_primeCounting, Polynomial.degree_pow_le, Finset.grade_eq, exists_seq_strictAnti_tendsto', cauchySeq_iff', Int.strictAntiOn_natAbs, ENNReal.tendsto_nat_tsum, IsCyclotomicExtension.discr_odd_prime, Polynomial.zero_le_degree_iff, exists_seq_strictMono_tendsto_nhdsWithin, PNat.Ioo_eq_finset_subtype, CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial, le_addRothNumber_product, ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum, MeasureTheory.monotone_spanningSets, Behrend.roth_lower_bound_explicit, Filter.Tendsto.partialSups_apply, CircleDeg1Lift.tendsto_translationNumber_aux, Function.iterate_injOn_Iio_minimalPeriod, sortedLT_map_fst_divisorsAntidiagonalList, Polynomial.mod_eq_self_iff, cyclotomicCharacter.toZModPow, Fin.finsetImage_val_Ioi, SimplexCategory.δ_comp_σ_of_gt'_assoc, Finset.prod_Ico_consecutive, AkraBazziRecurrence.isBigO_apply_r_sub_b, MeasureTheory.measure_setOf_frequently_eq_zero, PowerSeries.degree_weierstrassMod_lt, add_pow_prime_pow_eq, image_sub_const_Ico, preimage_Ioi, disjointed_zero, lowerCentralSeries_antitone, AkraBazziRecurrence.rpow_p_mul_one_add_smoothingFn_ge, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos_assoc, LocallyFinite.exists_forall_eventually_atTop_eventually_eq', Fin.attachFin_Ioo_eq_Ioi, nth_monotone, NNReal.tendsto_dist_agmSequences_atTop_zero, exists_seq_strictAnti_tendsto, edist_le_Ico_sum_of_edist_le, Finset.prod_range_mul_prod_Ico, MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm, upperCentralSeries_mono, Polynomial.degree_gcd_le_left, rothNumberNat_le, partialSups_eq_sup'_range, monotone_primeCounting', ExpGrowth.expGrowthInf_le_iff, schnirelmannDensity_le_iff_forall, AkraBazziRecurrence.dist_r_b', Finset.sum_Ico_sub, Fin.finsetImage_val_Ioo, preimage_Iio, tendsto_nat_floor_mul_atTop, IsArtinian.eventuallyConst_of_isArtinian, Finset.sum_condensed_le, le_schnirelmannDensity_iff, NormedAddCommGroup.summable_imp_tendsto_iff_completeSpace, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone, tendsto_birkhoffAverage_apply_sub_birkhoffAverage, cauchySeq_of_edist_le_of_tsum_ne_top, Multiset.Icc_eq, RootPairing.Iic_chainTopCoeff_eq, Order.height_nat, setOf_liouvilleWith_subset_aux, IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two, WellFoundedGT.iSup_eq_monotonicSequenceLimit, MeasureTheory.lowerCrossingTime_lt_upperCrossingTime, CategoryTheory.isArtinianObject_iff_not_strictAnti, ENat.monotone_map_iff, MeasureTheory.isProjectiveLimit_nat_iff, ENNReal.tendsto_pow_atTop_nhds_zero_iff, NNReal.tendsto_atTop_zero_of_summable, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', biUnion_range_succ_disjointed, Polynomial.length_coeffList_eq_withBotSucc_degree, Polynomial.degree_le_of_dvd, HasSumUniformly.tendstoUniformlyOn_finsetRange, frequently_atTop_modEq_one, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn, frequently_atTop_fermatPsp, Ico_image_const_sub_eq_Ico, mapClusterPt_neg_atTop_nsmul, LinearEquiv.dilatransvections_pow_mono, NNReal.not_summable_iff_tendsto_nat_atTop, nth_strictMono, tendstoUniformly_tsum_nat, List.toFinset_range'_1, SimpleGraph.antitoneOn_extremalNumber_div_choose_two, LinearMap.eventually_iSup_ker_pow_eq, MeasureTheory.not_frequently_of_upcrossings_lt_top, Partition.tendsto_order_genFun_term_atTop_nhds_top, Polynomial.div_tendsto_zero_iff_degree_lt, List.get_eq_get_rotate, preimage_Ici, MeasureTheory.BorelCantelli.martingalePart_process_ae_eq, Polynomial.degree_lt_degree_mul_X, MeasureTheory.Conservative.frequently_measure_inter_ne_zero, Polynomial.Splits.degree_le_one_of_irreducible, Set.ncard_Ioo_nat, inv_pow_anti, Set.ncard_Ico_nat, Behrend.bound_aux', isClosed_setOf_tendsto_birkhoffAverage, Fin.castLE_natCast, Finset.coe_range, Polynomial.divByMonic_eq_zero_iff, inv_pow_strictAnti, Partition.toFinsuppAntidiag_mem_finsuppAntidiag, MeasureTheory.upcrossingsBefore_zero', MvPolynomial.pow_idealOfVars, coeff_minpolyDiv_sub_pow_mem_span, MvPolynomial.idealOfVars_eq_restrictSupportIdeal, Finset.prod_Ico_reflect, image_cast_int_Icc, Fin.preimage_val_Ioc_val, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn, Function.antitone_iterate_of_le_id, image_cast_int_Iic, bitIndices_sorted, Filter.liminf_eq_iSup_iInf_of_nat', tendsto_self_mul_const_pow_of_lt_one, MeasureTheory.FinStronglyMeasurable.tendsto_approx, mulRothNumber_map_mul_left, ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_aux, factorization_factorial, Set.ncard_Iio_nat, spectrum.spectralRadius_le_liminf_pow_nnnorm_pow_one_div, tendstoUniformly_iff_seq_tendstoUniformly, cauchySeq_of_le_geometric, Prime.emultiplicity_factorial, LightProfinite.proj_comp_transitionMapLE', minpoly.degree_pos, Real.tendsto_eulerMascheroniSeq', Ico_pow_dvd_eq_Ico_of_lt, SimplexCategory.const_subinterval_eq, Filter.bliminf_eq_iSup_biInf_of_nat, HasFPowerSeriesOnBall.tendsto_partialSum_prod, strictMono_nat_of_lt_succ, exists_of_schnirelmannDensity_eq_zero, AkraBazziRecurrence.eventually_one_sub_smoothingFn_gt_const, Polynomial.tendsto_atTop_iff_leadingCoeff_nonneg, Chebyshev.psi_eq_sum_theta, Polynomial.degree_list_prod_le, Finset.pow_right_monotone, monotone_add_nat_iff_monotoneOn_nat_Ici, Real.Wallis.tendsto_W_nhds_pi_div_two, MeasureTheory.spanningSetsIndex_eq_iff, monotone_add_nat_of_le_succ, Chebyshev.psi_sub_theta_eq_sum_not_prime, AkraBazziRecurrence.eventually_bi_mul_le_r, NNReal.eventually_pow_one_div_le, MonomialOrder.toSyn_strictMono, HasSum.tendsto_sum_nat, Finset.le_sum_condensed', IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two, SequentiallyComplete.seq_is_cauchySeq, LinearGrowth.frequently_mul_le, image_cast_int_Ioc, FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop, Multipliable.hasProd_iff_tendsto_nat, Lagrange.eq_interpolate_iff, SeqCompactSpace.tendsto_subseq, SSet.iSup_skeleton, AkraBazziRecurrence.eventually_log_b_mul_pos, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, MeasureTheory.limsup_lintegral_le, tendsto_card_div_pow_atTop_volume, modularCyclotomicCharacter.pow_dvd_aux_pow_sub_aux_pow, Filter.eventually_iff_seq_eventually, eVariationOn.nonempty_monotone_mem, Dynamics.coverMincard_monotone_time, LTSeries.head_range, SummationFilter.conditional_filter_eq_map_range, Finset.pow_right_strictMonoOn, CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map, range_succ_eq_Iic, IsCyclotomicExtension.Rat.discr_prime_pow', Polynomial.degree_pos_of_root, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two, EulerProduct.eulerProduct_completely_multiplicative, eventually_pow_lt_factorial_sub, frequently_atTop_iff_infinite, MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq, preimage_Ioc, PowerSeries.degree_trunc_lt, Polynomial.card_roots_map_le_degree, CategoryTheory.Functor.ofSequence_map_homOfLE_succ, HasOuterApproxClosed.tendsto_apprSeq, Filter.HasBasis.exists_antitone_subbasis, PNat.tendsto_comp_val_iff, Cubic.degree_of_a_eq_zero', MeasureTheory.tendsto_integral_approxOn_of_measurable, GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite, preimage_Icc, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp, lightDiagramToLightProfinite_obj, DenseRange.exists_seq_strictMono_tendsto, closedBall_eq_Icc, finSigmaFinEquiv_apply, factorization_eq_card_pow_dvd_of_lt, AkraBazziRecurrence.sumTransform_def, mapClusterPt_atTop_nsmul_tfae, MeasureTheory.SimpleFunc.tendsto_eapprox, Pell.strictMono_y, mono_cast, PadicInt.fwdDiff_tendsto_zero, LocallyFinite.exists_forall_eventually_eq_prod, Filter.tendsto_iff_seq_tendsto, IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two, image_cast_int_Ici, SSet.skeleton_le_skeletonOfMono, Finset.prod_Icc_succ_top, ZLattice.covolume.tendsto_card_div_pow, ceil_mono, Polynomial.degree_mono, preimage_Ioo, AkraBazziRecurrence.tendsto_atTop_r, Polynomial.degree_C_lt_degree_C_mul_X, isTheta_choose, Polynomial.tendsto_atBot_iff_leadingCoeff_nonpos, MeasureTheory.BorelCantelli.predictablePart_process_ae_eq, IsTopologicalGroup.exists_antitone_basis_nhds_one, mulRothNumber_spec, derivedSeries_antitone, SimplexCategory.δ_comp_σ_of_gt', MeasureTheory.upperCrossingTime_bound_eq, LocallyFinite.exists_forall_eventually_atTop_eventuallyEq, Real.GammaSeq_tendsto_Gamma, Set.ncard_Iic_nat, FloorSemiring.tendsto_pow_div_factorial_atTop, List.toFinset_range'_1_1, tendsto_one_div_add_atTop_nhds_zero_nat, Finset.sum_Ico_eq_sub, LightProfinite.lightToProfinite_map_proj_eq, ProbabilityTheory.Kernel.martingale_densityProcess, frestrictLe_iterateInduction, Summable.tendsto_alternating_series_tsum, ProbabilityTheory.strong_law_ae, Fin.attachFin_Icc, MonotoneOn.integral_le_sum_Ico, IsTopologicalAddGroup.exists_antitone_basis_nhds_zero, cauchySeq_of_edist_le_of_summable, Monotone.monotone_iterate_of_le_map, AkraBazziRecurrence.isBigO_symm_asympBound, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc, minpoly.degree_le, MeasureTheory.MeasurePreserving.exists_mem_iterate_mem_of_measure_univ_lt_mul_measure, finPiFinEquiv_apply, ThreeAPFree.addRothNumber_eq, CategoryTheory.not_strictMono_of_isNoetherianObject, IsCyclotomicExtension.Rat.p_mem_span_zeta_sub_one, MeasureTheory.Measure.map_piSingleton, integral_le_sum_mul_Ico_of_antitone_monotone, Polynomial.abs_tendsto_atTop_iff, EulerProduct.eulerProduct, PNat.Ico_eq_finset_subtype, mapClusterPt_self_zsmul_atTop_nsmul, AddCircle.exists_norm_nsmul_le, isEquivalent_choose, PowerSeries.IsWeierstrassDivisionAt.degree_lt, Fin.attachFin_Ico_eq_Ici, Polynomial.degree_lt_wf, primorial_add, WithAbs.tendsto_one_div_one_add_pow_nhds_one, Valued.tendsto_zero_pow_of_le_exp_neg_one, Dense.exists_seq_strictAnti_tendsto_of_lt, clog_antitone_left, IsOpen.exists_iUnion_isClosed, Polynomial.degree_cubic_lt, mapClusterPt_atTop_zsmul_iff_nsmul, Cardinal.toNat_monotoneOn, not_strictMono_of_wellFoundedGT, mapClusterPt_self_atTop_pow, MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff, NNReal.tendsto_agmSequences_snd_agm, sum_mul_eq_sub_integral_mul', ENNReal.eventually_pow_one_div_le, DenseRange.exists_seq_strictMono_tendsto_of_lt, Polynomial.Sequence.natDegree_strictMono, Polynomial.degree_modByMonic_le, Finset.biUnion_slice, ContinuousWithinAt.partialSups_apply, addRothNumber_union_le, Valued.tendsto_zero_pow_of_v_lt_one, cauchySeq_of_edist_le_geometric_two, Urysohns.CU.approx_mono, LightProfinite.continuous_iff_convergent, OrderedSemiring.toPosSMulMonoNat, Finset.nsmul_right_monotone, antitone_add_nat_iff_antitoneOn_nat_Ici, Stirling.stirlingSeq'_antitone, Fin.preimage_val_Ioi_val, Polynomial.natDegree_lt_natDegree_iff, Commute.add_pow_prime_pow_eq, LTSeries.range_apply, pow_injOn_Iio_orderOf, MeasureTheory.Measure.pi_prod_map_IocProdIoc, Fin.isAddFreimanIso_Iic, MeasureTheory.crossing_pos_eq, EisensteinSeries.tendsto_zero_inv_linear_sub, PNat.natPred_monotone, AkraBazziRecurrence.isTheta_smoothingFn_sub_self, Summable.tendsto_atTop_zero, Fin.finsetImage_val_Iio, strictMono_mersenne, choose_mono, SummationFilter.hasSum_symmetricIoc_int_iff, CharP.natCast_injOn_Iio, ProbabilityTheory.measurableSet_partitionFiltration_of_mem, IsGLB.exists_seq_strictAnti_tendsto_of_notMem, Polynomial.coeffList_eraseLead, Ioc_filter_dvd_card_eq_div, fib_mono, tendsto_PNat_val_atTop_atTop, Polynomial.degree_divX_lt, MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset, Asymptotics.isBigO_nat_atTop_iff, Chebyshev.sum_PrimePow_eq_sum_sum, MvPowerSeries.coeff_inv, Polynomial.degree_eraseLead_lt, Complex.tendsto_one_add_div_pow_exp, ENNReal.tendsto_atTop_zero_of_tsum_ne_top, spectrum.gelfand_formula, tendsto_pow_atTop_nhds_zero_iff_norm_lt_one, partialSups_eq_sup_range, MeasureTheory.stoppedValue_lowerCrossingTime, AkraBazziRecurrence.tendsto_atTop_r_real, Polynomial.degree_X_pow_le, Finset.geomSum_ofColex_strictMono, Real.strictMono_eulerMascheroniSeq, finRotate_of_lt, Real.exists_seq_rat_strictAnti_tendsto, Polynomial.Chebyshev.strictAntiOn_node, tendsto_logDeriv_euler_sin_div, AkraBazziRecurrence.eventually_asympBound_pos, Polynomial.degree_monomial_le, mapClusterPt_one_atTop_pow, Prime.emultiplicity_choose', Polynomial.natDegree_lt_iff_degree_lt, Filter.subseq_tendsto_of_neBot, SummationFilter.hasSum_symmetricIcc_iff, Finset.sort_range, Lagrange.degree_interpolate_erase_lt, MeasureTheory.ae_eventually_notMem, Ioc_eq_range', CategoryTheory.Limits.SequentialProduct.functorMap_commSq_aux, rothNumberNat_zero, ZMod.card_units, Fin.image_val_Ici, Finset.tendsto_Ioo_neg, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg_assoc, Fin.addRothNumber_eq_rothNumberNat, clog_monotone, range_eq_Icc_zero_sub_one, HasSumLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange, Real.tendsto_harmonic_sub_log, instPosSMulMonoNatOfIsOrderedAddMonoid, IsMulFreimanHom.mulRothNumber_mono, frequently_atTop_prime_and_modEq, AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos, ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, Polynomial.degree_quadratic_le, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two', CircleDeg1Lift.tendsto_translation_number', MeasureTheory.upperCrossingTime_lt_lowerCrossingTime, Lagrange.degree_interpolate_lt, ZMod.sum_mul_div_add_sum_mul_div_eq_mul, comap_cast_atTop, padicValNat_choose', List.formPerm_apply_getElem, SeminormedAddCommGroup.cauchySeq_of_le_geometric, MeasureTheory.lintegral_liminf_le, Fin.image_val_Ioc, Polynomial.abs_tendsto_atBot_iff, Polynomial.degree_X_le, Prime.pow_dvd_factorial_iff, SSet.skeleton_obj_eq_top, sum_Ico_le_integral_of_le, controlled_sum_of_mem_closure_range, ENNReal.tendsto_pow_atTop_nhds_top_iff, CategoryTheory.Functor.ofOpSequence_obj, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, MeasureTheory.tendsto_indicator_ge, ProbabilityTheory.Kernel.partialTraj_succ_eq_comp, Summable.hasSum_iff_tendsto_nat, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι, Submodule.finrank_strictMono, exists_seq_strictAnti_strictMono_tendsto, Finset.sum_card_slice, tendsto_natCast_div_add_atTop, Polynomial.degree_derivative_lt, minpoly.degree_le_of_ne_zero, ProbabilityTheory.Kernel.partialTraj_le_def, Filter.eventuallyConst_atTop_nat, div_eq_quo_add_sum_rem_div, CompleteLatticeHom.apply_liminf_iterate, MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset, AkraBazziRecurrence.eventually_r_lt_n, tendstoUniformlyOn_tsum_nat, Set.ncard_Icc_nat, FormalMultilinearSeries.compPartialSumTarget_tendsto_atTop, PowerBasis.mem_span_pow', ProbabilityTheory.Kernel.memL1_limitProcess_densityProcess, geom_sum_Ico_mul, Real.strictAnti_eulerMascheroniSeq', ProbabilityTheory.measurable_countablePartitionSet_subtype, FormalMultilinearSeries.radius_inv_eq_limsup, IsPrimitiveRoot.finite_quotient_span_sub_one', spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius, geom_sum_Ico_mul_neg, succ_eq_succ, Finset.sum_Ico_succ_top, Finset.intervalGapsWithin_surjOn, RCLike.tendsto_add_mul_div_add_mul_atTop_nhds, ThreeGPFree.le_mulRothNumber, preimage_Iic, PNat.map_subtype_embedding_Icc, Multipliable.tendsto_atTop_one, intervalIntegral.sum_integral_adjacent_intervals_Ico, eventually_pos, tendsto_arithGeom_nhds_of_lt_one, LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_pos, AntitoneOn.sum_le_integral_Ico, Prime.emultiplicity_choose, IsPrimitiveRoot.finite_quotient_span_sub_one, HasProd.tendsto_prod_nat, Ioc_filter_modEq_card, Polynomial.degree_erase_lt, Finset.Nonempty.card_nsmul_mono, addRothNumber_spec, Polynomial.degree_le_of_natDegree_le, card_Ioo, TruncatedWittVector.truncate_truncate, MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre_nat, tendstoUniformlyOn_iff_seq_tendstoUniformlyOn, Fin.preimage_val_Iic_val, SSet.mem_skeleton_obj_iff_of_nonDegenerate, LinearGrowth.linearGrowthSup_le_iff, IsArtinian.monotone_stabilizes, MeasureTheory.inducedFamily_Iic, RingSeminorm.isBoundedUnder, exists_seq_tendsto_sSup, Fin.finsetImage_val_Ioc, Set.nsmul_right_monotone, MeasureTheory.Measure.pi_prod_map_IicProdIoc, IsDiscreteValuationRing.bot_lt_toWithBotNat_iff, ProbabilityTheory.Kernel.measurable_countableFiltration_densityProcess, card_Iic, MeasureTheory.measurableCylinders_nat, partialSups_eq_sUnion_image, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt'_assoc, PNat.equivNonZeroDivisorsNat_symm_apply_coe, Fin.preimage_val_Ico_val, LightProfinite.Extend.functor_map, frequently_odd, NNRat.tendsto_inv_atTop_nhds_zero_nat, Fin.val_strictMono, Finset.intervalGapsWithin_injOn, Polynomial.degree_sum_le, Polynomial.degree_pos_of_ne_zero_of_nonunit, withBotSucc_zero, tendsto_pow_const_mul_const_pow_of_abs_lt_one, HasSumLocallyUniformly.tendstoLocallyUniformly_finsetRange, Fin.map_valEmbedding_Ici, List.getElem_rotate, monotoneOn_nat_Ici_of_le_succ, EReal.tendsto_const_div_atTop_nhds_zero_nat, gc_count_nth, MonotoneOn.sum_le_integral_Ico, Filter.Eventually.natCast_atTop, CategoryTheory.Functor.OfSequence.map_comp_assoc, Irreducible.degree_pos, addRothNumber_le_ruzsaSzemerediNumber, IsCyclotomicExtension.Rat.discr_prime_pow_ne_two', ENNReal.tendsto_nat_nhds_top, ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj, Set.sum_indicator_eventually_eq_card, tendsto_integral_mul_one_add_inv_smul_sq_pow, Polynomial.Monic.degree_pos, Fin.image_val_Iio, NNReal.agmSequences_fst_monotone, log_antitone_left, mapClusterPt_self_zpow_atTop_pow, sum_mul_Ico_le_integral_of_monotone_antitone, preCantorSet_antitone, LieModule.antitone_lowerCentralSeries, AddChar.tendsto_eval_one_sub_pow, DyckWord.monotone_semilength, Filter.exists_seq_antitone_tendsto_atTop_atBot, Complex.tendsto_euler_sin_prod, MeasureTheory.stoppedValue_upperCrossingTime, Cardinal.toNat_strictMonoOn, Filter.extraction_forall_of_eventually', tendsto_arithGeom_atTop_of_one_lt, sum_Ioo_inv_sq_le, sum_mul_eq_sub_integral_mul₀', succPNat_strictMono, eventually_norm_pow_le, Polynomial.degree_le_natDegree, LinearMap.iterateKer_coe, addRothNumber_empty, MeasureTheory.partialTraj_const, Filter.antitone_seq_of_seq, CategoryTheory.antitone_chain_condition_of_isArtinianObject, Ico_filter_modEq_card, SSet.skeleton_succ, cauchySeq_of_dist_le_of_summable, FormalMultilinearSeries.isLittleO_one_of_lt_radius, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, rothNumberNat_def, ack_mono_right, ProbabilityTheory.Kernel.partialTraj_le, Polynomial.degree_divByMonic_le, Polynomial.degree_le_mul_left, addRothNumber_lt_of_forall_not_threeAPFree, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn', NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat, PowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent, ProbabilityTheory.Kernel.density_ae_eq_limitProcess, tendsto_nat_ceil_atTop, IsCyclotomicExtension.discr_prime_pow_ne_two, Polynomial.exists_multiset_roots, Ideal.mem_leadingCoeffNth, Function.Injective.nat_tendsto_atTop, pred_eq_pred, count_monotone, Set.isPWO_iff_exists_monotone_subseq, mapClusterPt_zero_atTop_nsmul, AkraBazziRecurrence.eventually_one_sub_smoothingFn_r_pos, ProbabilityTheory.strong_law_aux6, mapClusterPt_atTop_zpow_iff_pow, MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd, sum_Ico_pow, Polynomial.degree_C_lt, Finset.sum_Ico_by_parts, HasFPowerSeriesOnBall.tendstoUniformlyOn, ProbabilityTheory.Kernel.partialTraj_succ_self, LinearGrowth.tendsto_atTop_of_linearGrowthInf_pos, Subadditive.tendsto_lim, Polynomial.degree_C_mul_X_pow_le, exists_of_count_lt_count, exists_monotone_Icc_subset_open_cover_unitInterval_prod_self, WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, controlled_prod_of_mem_closure_range, MeasureTheory.SimpleFunc.tendsto_approxOn, HasProdLocallyUniformly.tendstoLocallyUniformly_finsetRange, IsPrimitiveRoot.finite_quotient_toInteger_sub_one, prod_Icc_factorial, Denumerable.raise'_sorted, isLittleO_pow_pow_of_abs_lt_left, card_Icc, Summable.tendsto_sum_tsum_nat, MonomialOrder.toSyn_monotone, CategoryTheory.isEventuallyConstant_of_isArtinianObject, Polynomial.degree_intCast_le, Fin.finsetImage_val_Ico, Fin.attachFin_uIcc, Polynomial.div_eq_zero_iff, NNReal.tendsto_sum_nat_add, ContractingWith.tendsto_iterate_efixedPoint, MeasureTheory.stronglyAdapted_predictablePart', MvPowerSeries.coeff_inv_aux, PNat.map_subtype_embedding_Ioo, Liouville.frequently_exists_num, Set.limsup_eq_tendsto_sum_indicator_atTop, multiplicity_choose_aux, tendsto_div_const_atTop, Set.pow_right_monotone, WithBot.lt_zero_iff, Polynomial.exists_degree_le_of_mem_span, Ordinal.one_add_natCast, Commute.geom_sum₂_Ico, IsPrimitiveRoot.norm_toInteger_sub_one_eq_one, rothNumberNat_isLittleO_id, AntitoneOn.integral_le_sum_Ico, instIsOrderBornology, ArithmeticFunction.sum_Ioc_zeta, HasProdUniformlyOn.tendstoUniformlyOn_finsetRange, gc_ceil_coe, ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filter, MeasureTheory.upperCrossingTime_lt_bddAbove, tendsto_pow_atTop_atTop_of_one_lt, Ideal.Filtration.antitone, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver', Filter.frequently_iff_seq_forall, MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm', List.monotone_sum_take, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', LinearEquiv.transvections_pow_mono, ThreeAPFree.le_rothNumberNat, tendsto_smoothingFun_of_map_one_le_one, MvPowerSeries.coeff_trunc, mem_add_wellApproximable_iff, Polynomial.eraseLead_degree_le, FloorSemiring.gc_ceil, addRothNumber_singleton, CategoryTheory.Functor.ofOpSequence_map_homOfLE_succ, Finset.prod_Ico_id_eq_factorial, Filter.isCountablyGenerated_iff_exists_antitone_basis, Finset.sum_Ico_Ico_comm, Fin.finsetImage_val_Ici, tendsto_self_mul_const_pow_of_abs_lt_one, PNat.Ioc_eq_finset_subtype, Polynomial.degree_X_sub_C_le, ArithmeticFunction.IsMultiplicative.eulerProduct, MeasurableSet.measurableSet_bliminf, HasFPowerSeriesAt.tendsto_partialSum_prod_of_comp, tendsto_fib_div_fib_succ_atTop, List.formPerm_pow_apply_getElem, antitoneOn_nat_Ici_of_succ_le, ContractingWith.exists_fixedPoint, MeasureTheory.tendsto_ae_condExp, Polynomial.degree_C_mul_X_le, mem_Ioc_succ', Ico_filter_modEq_cast, sum_Icc_choose, card_Ico, Fin.map_valEmbedding_Icc, Finset.intervalGapsWithin_pairwiseDisjoint_Ioc, ENNReal.tsum_eq_limsup_sum_nat, MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone', instIsSuccArchimedean, setOf_pow_dvd_eq_Icc_factorization, Ico_pred_singleton, IsMulFreimanIso.mulRothNumber_congr, CategoryTheory.monotone_chain_condition_of_isNoetherianObject, Polynomial.degree_wronskian_lt_add, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one', Fin.attachFin_Ico, factorization_choose', withBotSucc_one, IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one, ProbabilityTheory.measurableSet_partitionFiltration_memPartitionSet, sum_mul_eq_sub_integral_mul₁, SimplexCategoryGenRel.IsAdmissible.sorted, Chebyshev.psi_eq_theta_add_sum_theta, ContinuousWithinAt.partialSups, Filter.map_sub_atTop_eq_nat, ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range, spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius, ZMod.gauss_lemma, LiouvilleWith.frequently_lt_rpow_neg, AkraBazziRecurrence.eventually_asympBound_r_pos, IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two, WithBot.one_le_iff_zero_lt, schnirelmannDensity_le_div, le_mulRothNumber_product, Finset.nsmul_right_strictMono, tendsto_nat_floor_atTop, HasFPowerSeriesOnBall.tendstoUniformlyOn', MeasureTheory.upperCrossingTime_lt_nonempty, PadicInt.continuousAddCharEquiv_of_norm_mul_symm_apply, add_pow_prime_eq, ContinuousOn.partialSups, MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing, Polynomial.degree_one_le, Filter.liminf_eq_iSup_iInf_of_nat, mem_closure_iff_seq_limit, ProbabilityTheory.measurableSet_countableFiltration_countablePartitionSet, Polynomial.Chebyshev.isLocalExtr_T_real_iff, HasFPowerSeriesWithinOnBall.tendsto_partialSum_prod, Set.ncard_Ioc_nat, ContractingWith.tendsto_iterate_fixedPoint, pow_right_monotone, NormedAddCommGroup.exists_norm_nsmul_le, CauSeq.tendsto_limit, Icc_factorization_eq_pow_dvd, Polynomial.tendsto_nhds_iff, tendsto_pow_atTop_atTop_of_one_lt, SummationFilter.hasProd_symmetricIco_int_iff, monotone_factorial, SummationFilter.hasSum_symmetricIco_int_iff, MeasureTheory.upcrossingsBefore_le, Finset.prod_eq_prod_Ico_succ_bot, tendsto_add_mul_div_add_mul_atTop_nhds, Dynamics.netMaxcard_monotone_time, Cubic.degree_of_a_eq_zero, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, tendsto_one_div_atTop_nhds_zero_nat, tendsto_nhds_iff_seq_tendsto, ThreeAPFree.le_addRothNumber, tendsto_pow_atTop_nhds_zero_of_abs_lt_one, CategoryTheory.isNoetherianObject_iff_monotone_chain_condition, xInTermsOfW_vars_subset, SchwartzMap.eLpNorm_le_seminorm, Finset.sum_Ioc_succ_top, tendsto_natCast_atTop_iff, MeasureTheory.SimpleFunc.monotone_eapprox, MeasureTheory.measure_liminf_atTop_eq_zero, NNReal.hasSum_iff_tendsto_nat, TopologicalSpace.FirstCountableTopology.tendsto_subseq, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj, Cubic.equiv_symm_apply_b, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, le_monotonicSequenceLimit, image_cast_int_Ioi, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_pos, IsCyclotomicExtension.Rat.eq_span_zeta_sub_one_of_liesOver, CauSeq.cauchySeq, Finset.sum_eq_sum_Ico_succ_bot, nth_injOn, Filter.tendsto_finset_range, antitone_add_nat_of_succ_le, MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm, MeasureTheory.NullMeasurableSet.disjointed, cauchySeq_iff_le_tendsto_0, summable_iff_not_tendsto_nat_atTop_of_nonneg, ContinuousAt.partialSups, ExpGrowth.le_expGrowthInf_iff, LightProfinite.Extend.functorOp_map, mapClusterPt_self_atTop_nsmul, StrictOrderedSemiring.toSMulPosStrictMonoNat, AkraBazziRecurrence.eventually_one_sub_smoothingFn_nonneg, gaussSum_pow_eq_prod_jacobiSum_aux, HasFPowerSeriesOnBall.tendsto_partialSum, Finset.prod_Ico_eq_div, partialSups_zero, NNReal.agmSequences_monotone_and_antitone, FirstOrder.Language.BoundedFormula.castLE_comp_castLE, factorial_tendsto_atTop, wellFoundedGT_iff_monotone_chain_condition, LinearMap.eventually_isCompl_ker_pow_range_pow, MeasureTheory.mem_disjointed_spanningSetsIndex, mulRothNumber_empty, Polynomial.Splits.splits, Finset.Nonempty.card_pow_mono, minpoly.IsIntegrallyClosed.degree_le_of_ne_zero, HasOuterApproxClosed.tendsto_lintegral_apprSeq, Function.Bijective.cauchySeq_comp_iff, Polynomial.degree_prod_le, Module.End.eventually_disjoint_ker_pow_range_pow, monotone_stabilizes_iff_noetherian, HasSumUniformlyOn.tendstoUniformlyOn_finsetRange, MeasurableSet.measurableSet_liminf, Polynomial.div_eq_quo_add_rem_div, BoxIntegral.Box.exists_seq_mono_tendsto, PowerSeries.trunc_apply, Polynomial.degree_zero_le, Polynomial.Monic.degree_pos_of_not_isUnit, Fin.attachFin_Ioo, Finset.sum_Ico_eq_sum_range, nsmul_left_monotone, Finset.tendsto_Icc_neg, ENNReal.tendsto_inv_nat_nhds_zero, Behrend.card_sphere_le_rothNumberNat, cauchySeq_of_edist_le_geometric, Multiset.card_mono, Polynomial.isBoundedUnder_abs_atBot_iff, Stirling.log_stirlingSeq'_antitone, ExpGrowth.frequently_le_exp, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two, MeasureTheory.OuterMeasure.mkMetric'.mono_pre_nat, Summable.tendsto_atTop_of_pos, TruncatedWittVector.truncate_comp, rothNumberNat_le_ruzsaSzemerediNumberNat, pow_right_strictAnti₀, ZLattice.covolume.tendsto_card_div_pow', isCauSeq_iff_cauchySeq, MeasureTheory.tendsto_eLpNorm_condExp, Asymptotics.isBigO_one_nat_atTop_iff, MeasureTheory.Conservative.measure_inter_frequently_image_mem_eq, EisensteinSeries.tendsto_zero_inv_linear, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos, Asymptotics.IsBigO.natCast_atTop, Polynomial.degree_pos_of_not_isUnit_of_dvd_monic, Ico_eq_range', Fin.map_valEmbedding_Ioi, fib_strictMonoOn, IsPrimitiveRoot.toInteger_sub_one_dvd_prime, ProbabilityTheory.iSup_countableFiltration, padicValNat_choose, antitone_nat_of_succ_le, HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange, MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd, tendsto_logDeriv_euler_cot_sub, PNat.mk_ofNat, List.monotone_prod_take, mem_wellApproximable_iff, Fin.finsetImage_val_Icc, Chebyshev.theta_eq_sum_Icc, Fin.image_val_Ioi, Lagrange.degree_interpolate_le, riemannZeta_eulerProduct, tendsto_algebraMap_inverse_atTop_nhds_zero_nat, smallSchroder_succ, ExpGrowth.frequently_exp_le, LieModule.chainTopCoeff_add_one, minpoly.min, sortedGT_map_snd_divisorsAntidiagonalList, padicValNat_factorial, controlled_sum_of_mem_closure, AkraBazziRecurrence.eventually_atTop_sumTransform_le, LTSeries.last_range, mul_geom_sum₂_Ico, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two, SSet.skeletonOfMono_zero, pow_monotoneOn, monotone_primeCounting, ProbabilityTheory.Kernel.tendsto_setIntegral_densityProcess, YoungDiagram.equivListRowLens_apply_coe, Polynomial.mem_closure_X_union_C, tendsto_natCast_atTop_atTop, ProbabilityTheory.Kernel.stronglyMeasurable_countableFiltration_densityProcess, addRothNumber_map_add_left, List.sorted_le_range', tendsto_mod_div_atTop_nhds_zero_nat, pow_right_mono₀, rothNumberNat_add_le, numDerangements_tendsto_inv_e, LiouvilleWith.exists_pos, Fin.map_valEmbedding_Ioo, Filter.exists_seq_monotone_tendsto_atTop_atTop, disjointedRec_zero, MeasureTheory.upcrossingsBefore_eq_sum, AbsoluteValue.tendsto_div_one_add_pow_nhds_one, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt'_assoc, FormalMultilinearSeries.isLittleO_of_lt_radius, Measurable.liminf, IsPrimitiveRoot.toInteger_sub_one_dvd_prime', Polynomial.degree_multiset_prod_le, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, MeasureTheory.stoppedValue_sub_eq_sum, pow_right_anti₀, pow_left_strictMono, AkraBazziRecurrence.isEquivalent_smoothingFn_sub_self, AkraBazziRecurrence.eventually_atTop_sumTransform_ge, Polynomial.degree_sub_le, ProbabilityTheory.strong_law_aux7, AkraBazziRecurrence.exists_eventually_r_le_const_mul, Finset.prod_Ico_succ_top, Fin.take_succ_eq_snoc, fib_add_two_strictMono, Ico_filter_coprime_le, LinearGrowth.eventually_mul_le, LinearMap.eventually_iInf_range_pow_eq, Finset.sum_Ico_succ_sub_top, ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id, EulerSine.tendsto_integral_cos_pow_mul_div, Matrix.charpoly_sub_diagonal_degree_lt, CategoryTheory.Limits.IsFiltered.sequentialFunctor_final, ProbabilityTheory.Kernel.condExp_densityProcess, SimpleGraph.tendsto_turanDensity, mapClusterPt_atTop_pow_iff_mem_topologicalClosure_zpowers, ProbabilityTheory.Kernel.partialTraj_self, Real.tendsto_sum_range_one_div_nat_succ_atTop, LinearGrowth.frequently_le_mul, Polynomial.degree_smul_le, Ico_succ_right_eq_insert_Ico, ProbabilityTheory.Kernel.tendsto_densityProcess_limitProcess, CircleDeg1Lift.tendsto_translation_number₀, ENNReal.hasSum_iff_tendsto_nat, ProbabilityTheory.strong_law_Lp, Multiset.grade_eq, SSet.mem_skeleton, MvPowerSeries.coeff_truncFun, CStarAlgebra.pow_antitone, WithBot.lt_one_iff_le_zero, ContractingWith.exists_fixedPoint', Cubic.equiv_symm_apply_c, SSet.iSup_skeletonOfMono, PadicInt.appr_mono, localCohomology.ideal_powers_initial, ExpGrowth.eventually_exp_le, List.sortedLT_range', Order.coheight_nat, LieModule.eventually_genWeightSpace_smul_add_eq_bot, CategoryTheory.Functor.OfSequence.map_comp, MeasureTheory.SimpleFunc.tendsto_nearestPt, AkraBazziRecurrence.eventually_r_pos, OrderedSemiring.toSMulPosMonoNat, MeasurableSet.measurableSet_limsup, Fin.attachFin_Iio, divisorsAntidiagonal_eq_prod_filter_of_le, TruncatedWittVector.card_zmod, hyperfilter_le_atTop, PNat.equivNonZeroDivisorsNat_apply_coe, SSet.skeletonOfMono_obj_eq_top, Polynomial.degree_lt_degree, locallyIntegrableOn_mul_sum_Icc, Finset.Colex.erase_le_erase_min', Fin.map_valEmbedding_Ico, ENNReal.tendsto_sum_nat_add, CategoryTheory.isArtinianObject_iff_antitone_chain_condition, Filter.strictMono_subseq_of_id_le, Composition.ones_embedding, Polynomial.degree_le_iff_coeff_zero, add_pow_prime_pow_eq', Finset.sum_Ico_consecutive, MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd, IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one, Fin.addRothNumber_le_rothNumberNat, EisensteinSeries.tendsto_double_sum_S_act, filter_coprime_Ico_eq_totient, FloorSemiring.eventually_mul_pow_lt_factorial_sub, ThreeGPFree.mulRothNumber_eq, Polynomial.isBoundedUnder_abs_atTop_iff, AkraBazziRecurrence.dist_r_b, ack_strictMono_right, Polynomial.card_roots, mem_tangentConeAt_iff_exists_seq, Polynomial.ofFn_degree_lt, seminormFromConst_isLimit, Fin.preimage_val_Icc_val, IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two, HasFPowerSeriesWithinOnBall.tendstoUniformlyOn, AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc, ProbabilityTheory.Fernique.normThreshold_strictMono, HasFPowerSeriesAt.tendsto_partialSum, cyclotomicCharacter.toFun_apply, isLittleO_pow_pow_of_lt_left, Pell.strictMono_x, quadraticChar_odd_prime, Ico_zero_eq_range, spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius, Finset.prod_Ico_div, MeasureTheory.upcrossingsBefore_zero, Finset.sum_Icc_succ_top, MeasureTheory.StronglyMeasurable.tendsto_approx, Filter.exists_seq_forall_of_frequently, SimplexCategoryGenRel.IsAdmissible.pairwise, Set.partialSups_eq_accumulate, CategoryTheory.SimplicialObject.δ_comp_σ_of_gt', FormalMultilinearSeries.radius_right_inv_pos_of_radius_pos_aux1, isLittleO_coe_const_pow_of_one_lt, IsAddFreimanIso.addRothNumber_congr, NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one, cyclotomicCharacter.toZModPow_toFun, addRothNumber_le, nth_strictMonoOn, Polynomial.degree_modByMonic_lt, Finset.prod_Ioc_consecutive, MonotoneOn.exists_tendsto_deriv_liminf_lintegral_enorm_le, eventually_mul_pow_lt_factorial_sub, AlgebraicGeometry.Proj.SpecMap_awayMap_awayι, Composition.monotone_sizeUpTo, Filter.map_add_atTop_eq_nat, image_cast_int_Ioo, Polynomial.degree_lt_iff_coeff_zero, MvPowerSeries.coeff_invOfUnit, AkraBazziRecurrence.isBigO_asympBound, ProbabilityTheory.strong_law_aux4, strictMono_cast, HomogeneousLocalization.Away.eventually_smul_mem, Polynomial.div_tendsto_atBot_zero_iff_degree_lt, MeasureTheory.martingalePart_eq_sum, Dense.exists_seq_strictAnti_tendsto, legendreSym.card_sqrts, range_succ_eq_Icc_zero, SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate, ZMod.gauss_lemma_aux, NNReal.tendsto_inverse_atTop_nhds_zero_nat, Fin.range_val, LinearGrowth.le_linearGrowthInf_iff, AkraBazziRecurrence.eventually_r_ge, LSeriesSummable.isBigO_rpow, MeasurableSet.disjointed, MeasurableSet.measurableSet_blimsup, MeasureTheory.upperCrossingTime_eq_of_bound_le, div_eq_quo_add_rem_div_add_rem_div, Ico_filter_pow_dvd_eq, Filter.tendsto_add_atTop_iff_nat, DyckWord.strictMono_semilength, Polynomial.degree_le_zero_iff, IsAddFreimanHom.addRothNumber_mono, MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop, Set.infinite_iff_tendsto_sum_indicator_atTop, MeasureTheory.isPredictable_iff_measurable_add_one, MeasureTheory.measure_limsup_atTop_eq_zero, MeasureTheory.Conservative.inter_frequently_image_mem_ae_eq, Chebyshev.psi_eq_sum_Icc, MeasureTheory.exists_null_frontiers_thickening, Polynomial.degree_add_le, finPiFinEquiv_single, Real.BohrMollerup.tendsto_logGammaSeq, tendsto_pow_atTop_nhds_zero_of_lt_one, Real.tendsto_sum_pi_div_four, StrictMono.strictMono_iterate_of_lt_map, ModularFormClass.qExpansion_isBigO, card_Ioc, Fin.castPred_one, LinearMap.iterateRange_coe, harmonic_eq_sum_Icc, Polynomial.degree_pos_of_aeval_root, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two, gaussSum_pow_eq_prod_jacobiSum, Set.Icc.monotone_addNSMul, PNat.natPred_strictMono, add_pow_prime_eq', RootPairing.Iic_chainBotCoeff_eq, frequently_mod_eq, Fin.castLE_rfl, LTSeries.length_range, factorization_eq_card_pow_dvd, HasFPowerSeriesWithinOnBall.tendstoUniformlyOn', tendsto_pow_const_mul_const_pow_of_lt_one, ENNReal.tsum_eq_liminf_sum_nat, LinearGrowth.linearGrowthInf_le_iff, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, bernsteinApproximation_uniform, Polynomial.le_degree_of_ne_zero, integrableOn_mul_sum_Icc, CStarAlgebra.pow_monotone, strictAnti_nat_of_succ_lt, MeasureTheory.partialTraj_const_restrict₂, Filter.liminf_nat_add, MvPolynomial.psum_eq_mul_esymm_sub_sum, Cubic.equiv_apply_coe, MeasureTheory.exists_seq_tendstoInMeasure_atTop_iff, PairReduction.antitone_logSizeBallSeq_add_one_subset, integral_le_sum_Ico_of_le, Real.tendsto_eulerMascheroniSeq, geom_sum_Ico', ProbabilityTheory.measurableSet_countableFiltration_of_mem, Topology.RelCWComplex.FiniteDimensional.eventually_isEmpty_cell, AkraBazziRecurrence.rpow_p_mul_one_sub_smoothingFn_le, Multipliable.tendsto_prod_tprod_nat, eventuallyConst_of_isNoetherian, Fin.map_valEmbedding_univ, instSMulPosStrictMonoNatOfIsOrderedCancelAddMonoid, Ideal.pow_right_strictAnti, exists_seq_strictMono_tendsto, lightDiagramToLightProfinite_map, mulRothNumber_le, LinearGrowth.eventually_le_mul, Continuous.partialSups_apply, Polynomial.le_degree_of_mem_supp, Polynomial.degree_annIdealGenerator_le_of_mem, Finset.range_eq_Ico, cauchySeq_of_summable_dist, Set.seq_of_forall_finite_exists, Filter.exists_seq_tendsto, xInTermsOfW_vars_aux, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, AbsoluteValue.tendsto_div_one_add_pow_nhds_zero, ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection, schnirelmannDensity_lt_iff, Polynomial.abs_isBoundedUnder_iff, Monotone.antitone_iterate_of_map_le, not_summable_iff_tendsto_nat_atTop_of_nonneg, ENat.strictMono_map_iff, List.next_getElem, Subadditive.eventually_div_lt_of_div_lt, ProbabilityTheory.strong_law_aux1, Polynomial.natDegree_eq_zero_iff_degree_le_zero, ContinuousOn.partialSups_apply, fermatNumber_strictMono, Polynomial.degree_sub_lt, PowerSeries.isWeierstrassDivisionAt_iff, Fin.finsetImage_val_Iic, MeasureTheory.limsup_ae_eq_of_forall_ae_eq, Asymptotics.IsLittleO.natCast_atTop, Filter.limsup_eq_iInf_iSup_of_nat', monotone_stabilizes_iff_artinian, Ico_succ_singleton, tendsto_sum_nat_add, IsGLB.exists_seq_antitone_tendsto, Finset.sum_Ico_reflect, Finset.card_shatterer_le_sum_vcDim, floor_mono, ProbabilityTheory.strong_law_ae_simpleFunc_comp, Finset.prod_Ico_succ_div_top, Filter.tendsto_add_atTop_nat, SSet.δ_comp_σ_of_gt'_apply, eq_Ici_of_nonempty_of_upward_closed, Polynomial.degree_update_le, Finset.tendsto_Ico_neg, sum_Ioc_inv_sq_le_sub, tendsto_fib_succ_div_fib_atTop, Int.natCast_strictMono, Behrend.bound_aux, nth_eq_getD_sort, MeasureTheory.stronglyAdapted_predictablePart, Finset.prod_Ico_div_bot, Fin.image_val_Ico, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent, map_cast_int_atTop, cauchySeq_shift, Commute.mul_geom_sum₂_Ico, List.getElem_eq_getElem_rotate, Submodule.mem_iSup_of_chain, Icc_eq_range', Polynomial.Sequence.degree_strictMono, ProbabilityTheory.measurable_memPartitionSet_subtype, Polynomial.Monic.irreducible_iff_natDegree', Commute.add_pow_prime_eq, ProbabilityTheory.strong_law_aux2, frequently_even, ExpGrowth.expGrowthSup_le_iff, NNReal.agmSequences_snd_antitone, MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set, IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, Finset.tendsto_Ioc_neg, exists_monotone_Icc_subset_open_cover_unitInterval, Polynomial.degree_pos_of_irreducible, exists_seq_strictAnti_tendsto_nhdsWithin, tendsto_pow_const_div_const_pow_of_one_lt, WellFoundedGT.monotone_chain_condition', Cubic.degree_of_b_eq_zero', NNReal.summable_iff_not_tendsto_nat_atTop, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, Filter.zero_pow_eventuallyEq, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, SimplexCategoryGenRel.IsAdmissible.sortedLT, LinearMap.eventually_codisjoint_ker_pow_range_pow, ZMod.eisenstein_lemma, Finset.sum_Ioc_by_parts, Polynomial.degree_cubic_le, Finset.prod_Ioc_succ_top, ProbabilityTheory.iSup_partitionFiltration, ProbabilityTheory.strong_law_aux3, LieModule.eventually_iInf_lowerCentralSeries_eq, Finset.range_mono, Fin.preimage_val_Ioo_val, instSMulPosMonoNatOfIsOrderedAddMonoid, tendsto_add_one_pow_atTop_atTop_of_pos, Cubic.equiv_symm_apply_d, tendsto_atTop_of_geom_le, card_Iio, AkraBazziRecurrence.isTheta_asympBound, AkraBazziRecurrence.eventually_one_add_smoothingFn_r_pos, tendsto_primeCounting', CircleDeg1Lift.tendsto_translationNumber, ProbabilityTheory.strong_law_ae_real, Polynomial.degree_div_le, ArithmeticFunction.sum_Ioc_sigma0_eq_sum_div, multiset_Ico_map_mod, ProbabilityTheory.strong_law_aux5, Irreducible.degree_le_two, SimpleGraph.isEquivalent_extremalNumber, Real.tendsto_euler_sin_prod, MeasureTheory.tendsto_setToFun_approxOn_of_measurable, sum_mul_eq_sub_sub_integral_mul', Polynomial.degree_linear_le, CategoryTheory.Limits.SequentialProduct.cone_π_app, IsLUB.exists_seq_monotone_tendsto, FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2, MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, tendsto_inverse_atTop_nhds_zero_nat, CategoryTheory.Functor.ofSequence_obj, IsLUB.exists_seq_strictMono_tendsto_of_notMem, Int.strictMonoOn_natAbs, CategoryTheory.Limits.IsFiltered.sequentialFunctor_map, tendsto_seminormFromConst_seq_atTop, Continuous.partialSups, Multiset.toDFinsupp_lt_toDFinsupp, LightProfinite.Extend.functor_obj, exists_seq_tendsto_sInf, wellFoundedGT_iff_monotone_chain_condition', Filter.blimsup_eq_iInf_biSup_of_nat, Finset.intervalGapsWithin_mapsTo, one_div_pow_anti, Finset.prod_Ico_eq_prod_range, cofinite_eq_atTop, Filter.exists_antitone_basis, Polynomial.degree_linear_lt_degree_C_mul_X_sq, Polynomial.degree_cyclotomic_pos, Set.Finite.ncard_strictMonoOn, SummationFilter.symmetricIcc_eq_map_Icc_nat, IsPrimitiveRoot.zeta_sub_one_prime, Directed.sequence_anti, Polynomial.degree_pos_of_eval₂_root, YoungDiagram.equivListRowLens_symm_apply, Polynomial.withBotSucc_degree_eq_natDegree_add_one, MeasureTheory.upperCrossingTime_lt_succ, ContractingWith.tendsto_iterate_efixedPoint', sum_mul_eq_sub_integral_mul, LightProfinite.proj_surjective, partialSups_eq_biUnion_range, addRothNumber_Ico, Filter.exists_antitone_seq, UniformSpace.has_seq_basis, Polynomial.degree_quadratic_lt_degree_C_mul_X_cb, factorization_choose, HasProdUniformly.tendstoUniformlyOn_finsetRange, Filter.limsup_eq_iInf_iSup_of_nat, Cubic.degree_of_c_eq_zero, MvPolynomial.IsSymmetric.antitone_supDegree, Cubic.equiv_symm_apply_a, SimplexCategoryGenRel.simplicialEvalσ_monotone, LightProfinite.proj_comp_transitionMapLE, LightProfinite.instEpiAppOppositeNatπAsLimitCone, Function.monotone_iterate_of_id_le, FirstOrder.Language.BoundedFormula.realize_mapTermRel_add_castLe, List.chain'_iff_get, SzemerediRegularity.stepBound_mono, mem_tangentConeAt_iff_exists_seq_norm_tendsto_atTop, mulRothNumber_lt_of_forall_not_threeGPFree, preimage_find_eq_disjointed, PadicInt.continuousAddCharEquiv_apply, SummationFilter.hasProd_symmetricIcc_iff, AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_le_nat, cauchySeq_of_le_geometric_two, dist_le_Ico_sum_of_dist_le, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, ProbabilityTheory.measurable_partitionFiltration_memPartitionSet, edist_le_Ico_sum_edist, IsCyclotomicExtension.Rat.discr_odd_prime', CategoryTheory.Limits.SequentialProduct.functorMap_commSq_succ, TFAE_exists_lt_isLittleO_pow, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, ProbabilityTheory.strong_law_ae_of_measurable, PowerSeries.WithPiTopology.tendsto_trunc_atTop, List.sorted_lt_range', Polynomial.natDegree_pos_iff_degree_pos, ZMod.prod_Ico_one_prime, Real.tendsto_log_nat_add_one_sub_log, Polynomial.degree_mod_lt, Multiset.sort_range, ArithmeticFunction.sum_Ioc_mul_eq_sum_sum, Dynamics.dynEntourage_antitone, Commute.add_pow_prime_eq', addRothNumber_map_add_right, List.sortedLE_range', HasFPowerSeriesWithinOnBall.tendsto_partialSum, IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iff, MeasureTheory.lintegral_liminf_le', Fin.map_valEmbedding_Iio, mapClusterPt_atTop_nsmul_iff_mem_topologicalClosure_zmultiples, Polynomial.mem_degreeLE, rothNumberNat_le_ruzsaSzemerediNumberNat', tendsto_smoothingFun_of_eq_zero, isLittleO_pow_const_const_pow_of_one_lt, MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm, geom_sum_Ico, Dense.exists_seq_strictMono_tendsto_of_lt, Stirling.tendsto_stirlingSeq_sqrt_pi, geom_sum₂_Ico, ruzsaSzemerediNumberNat_asymptotic_lower_bound, cauchy_series_of_le_geometric, Dense.exists_seq_strictMono_tendsto, Polynomial.degree_sum_fin_lt, DFinsupp.toMultiset_lt_toMultiset, Finsupp.DegLex.monotone_degree, List.isChain_iff_get, CategoryTheory.instCountableCategoryNat, StrictOrderedSemiring.toPosSMulStrictMonoNat, Filter.tendsto_sub_atTop_nat, Polynomial.degree_map_lt, tendsto_algebraMap_inv_atTop_nhds_zero_nat, PNat.map_subtype_embedding_Ioc, Cubic.degree_of_c_eq_zero', Polynomial.natDegree_le_iff_degree_le, tendsto_const_div_pow, PowerSeries.HasSubst.eventually_coeff_pow_eq_zero, filter_multiset_Ico_card_eq_of_periodic, tendsto_euler_sin_prod', Polynomial.Sequence.basis_degree_strictMono, exists_seq_strictMono_tendsto', pow_right_strictMono', MeasureTheory.upcrossingsBefore_mono, MeasureTheory.mul_upcrossingsBefore_le, sum_mul_eq_sub_integral_mul₀, Finset.pow_right_strictMono, tendsto_subseq_of_bounded, CategoryTheory.isNoetherianObject_iff_not_strictMono, HasFPowerSeriesOnBall.tendstoLocallyUniformlyOn', mulRothNumber_map_mul_right, Filter.frequently_iff_seq_frequently, hasSum_iff_tendsto_nat_of_nonneg, MeasureTheory.tendsto_integral_norm_approxOn_sub, ZLattice.covolume.tendsto_card_div_pow'', tendsto_pow_atTop_nhds_zero_of_norm_lt_one, emultiplicity_eq_card_pow_dvd, CategoryTheory.isEventuallyConstant_of_isNoetherianObject, DirichletCharacter.LSeries_eulerProduct, CategoryTheory.isNoetherianObject_iff_isEventuallyConstant, Filter.map_div_atTop_eq_nat, atTop_hasAntitoneBasis_of_archimedean, DenseRange.exists_seq_strictAnti_tendsto_of_lt, isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt, ProbabilityTheory.Kernel.partialTraj_zero, MeasureTheory.upcrossings_lt_top_iff, tendsto_pow_atTop_nhds_zero_iff, Polynomial.IsUnitTrinomial.irreducible_aux1, tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn, CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg, MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed_set_eq, Polynomial.div_tendsto_atTop_zero_iff_degree_lt, MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint, WithBot.coe_nonneg, tendsto_factorial_div_pow_self_atTop, CompactSpace.tendsto_subseq, PowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_zero, Polynomial.coeff_divByMonic_X_sub_C, AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_ge_nat, CategoryTheory.isArtinianObject_iff_isEventuallyConstant, LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure, NNReal.tendsto_const_div_atTop_nhds_zero_nat, sum_mul_eq_sub_sub_integral_mul, ZMod.eisenstein_lemma_aux, MeasureTheory.upcrossingsBefore_pos_eq, List.sorted_le_range, mulRothNumber_union_le, ProbabilityTheory.Fernique.tendsto_normThreshold_atTop, YoungDiagram.rowLens_sorted, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two', mod_injOn_Ico, Iio_eq_range, mem_Ioc_succ, Real.tendsto_prod_pi_div_two, pow_self_mono, SchwartzMap.one_add_le_sup_seminorm_apply, Polynomial.degree_erase_le, Commute.geom_sum₂_Ico_mul, qExpansion_coeff_isBigO_of_norm_isBigO, LinearGrowth.le_linearGrowthSup_iff, ExpGrowth.le_expGrowthSup_iff, fermatNumber_mono, OnePoint.continuous_iff_from_nat, GenContFract.of_correctness_atTop_of_terminates, dist_le_Ico_sum_dist, nsmul_left_strictMono, LightProfinite.proj_comp_transitionMap', ack_mono_left, Complex.approx_Gamma_integral_tendsto_Gamma_integral, Set.ncard_strictMono, exists_strictMono_subsequence, Real.BohrMollerup.tendsto_logGammaSeq_of_le_one, Set.Nonempty.eq_Icc_iff_nat, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp, MeasureTheory.tendstoInMeasure_iff_tendsto_Lp_finite, MeasureTheory.SimpleFunc.monotone_approx, FormalMultilinearSeries.radius_eq_liminf, SummationFilter.hasProd_symmetricIoc_int_iff, MeasureTheory.exists_upperCrossingTime_eq, frequently_modEq, cauchySeq_iff, Filter.Tendsto.partialSups, FormalMultilinearSeries.compPartialSumTarget_tendsto_prod_atTop, greatestFib_mono, integral_sin_pow_antitone, ProbabilityTheory.measurable_countableFiltration_countablePartitionSet, Fin.image_val_Icc, mapClusterPt_inv_atTop_pow, Commute.add_pow_prime_pow_eq', HasOuterApproxClosed.exAppr, ZMod.div_eq_filter_card, Polynomial.degree_derivative_le, Multiset.toFinsupp_strictMono, AkraBazziRecurrence.eventually_r_le_b, Real.tendsto_harmonic_sub_log_add_one, Subgroup.IsSubnormal.isSubnormal_iff, nsmul_injOn_Iio_addOrderOf, Polynomial.mem_degreeLT, tendsto_inv_atTop_nhds_zero_nat, FirstOrder.Language.BoundedFormula.relabel_sumInl, Function.IsFixedPt.tendsto_birkhoffAverage, exists_strictAnti, Polynomial.Monic.degree_le_zero_iff_eq_one, MeasureTheory.SimpleFunc.tendsto_approxOn_Lp_eLpNorm, MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq, pow_right_strictMono₀, geom_sum_Ico_le_of_lt_one, FirstOrder.Language.DirectedSystem.natLERec.directedSystem, MeasureTheory.sum_restrict_disjointed_spanningSets, Finset.sum_condensed_le', PowerBasis.dim_le_degree_of_root, schnirelmannDensity_mul_le_card_filter, image_cast_int_Ico, Real.exists_seq_rat_strictMono_tendsto, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae', IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, Finset.prod_range_eq_mul_Ico, CircleDeg1Lift.tendsto_translation_number₀', Fin.preimage_val_Iio_val, geom_sum_Ico_le, ContinuousAt.partialSups_apply, Finset.sum_Ioc_consecutive, Ioo_eq_range', CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux, Finsupp.lt_wf, Finset.card_mono, MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le, Fin.castPred_zero, CategoryTheory.CosimplicialObject.δ_comp_σ_of_gt', Polynomial.degree_list_sum_le, DenseRange.exists_seq_strictAnti_tendsto, Fin.take_eq_self, Fin.map_valEmbedding_Iic, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two, Polynomial.degree_linear_lt, Finset.prod_Ico_eq_mul_inv, preimage_Ico, Polynomial.degree_natCast_le, ruzsaSzemerediNumberNat_mono, Directed.sequence_mono, Order.krullDim_nat, MeasureTheory.isProjectiveLimit_nat_iff', Polynomial.degree_modByMonic_le_left, MeasureTheory.Lp.cauchy_complete_eLpNorm, MeasureTheory.SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm, isBigO_pow_pow_of_le_left, instPosSMulStrictMonoNatOfIsOrderedAddMonoid, Real.BohrMollerup.tendsto_log_gamma, Multiset.card_strictMono, Real.tendsto_one_add_div_pow_exp, NNReal.tendsto_pow_atTop_nhds_zero_iff, Finset.sum_range_eq_add_Ico, Fin.map_valEmbedding_Ioc, tendsto_pow_atTop_nhdsWithin_zero_of_lt_one, IsCompact.tendsto_subseq, IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow', Dynamics.dynEntourage_eq_inter_Ico, List.sortedLT_range, IsCyclotomicExtension.discr_prime_pow, SSet.skeletonOfMono_succ, log_monotone, AkraBazziRecurrence.smoothingFn_mul_asympBound_isBigO_T, Denumerable.raise_sorted, Polynomial.exists_mul_add_mul_eq_C_resultant, Stirling.tendsto_self_div_two_mul_self_add_one, Fin.attachFin_Ioc, Submodule.coe_iSup_of_chain, Stirling.stirlingSeq_has_pos_limit_a, AkraBazziRecurrence.eventually_one_add_smoothingFn_nonneg, arithGeom_strictMono, IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two, Polynomial.roots_def, AddSubgroup.IsSubnormal.isSubnormal_iff, AkraBazziRecurrence.eventually_one_add_smoothingFn_pos, Subgroup.IsSubnormal.exists_chain, IsPrimitiveRoot.zeta_sub_one_prime', NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat, Behrend.map_monotone, AkraBazziRecurrence.eventually_b_le_r, mulRothNumber_singleton, Set.equitableOn_iff_exists_image_subset_icc, filter_Ico_card_eq_of_periodic, CategoryTheory.not_strictAnti_of_isArtinianObject, CategoryTheory.Limits.SequentialProduct.functorMap_commSq, Finset.nsmul_right_strictMonoOn, image_nth_Iio_card, IsCyclotomicExtension.discr_prime_pow_ne_two', degree_radical_le, AkraBazziRecurrence.isLittleO_self_div_log_id, Polynomial.degree_gcd_le_right, Polynomial.degree_C_le, not_strictAnti_of_wellFoundedLT, LinearGrowth.EReal.eventually_atTop_exists_nat_between, IsPrimitiveRoot.toInteger_sub_one_not_dvd_two, MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem, controlled_prod_of_mem_closure, tendsto_prod_nat_add, Fin.image_val_Ioo, instIsPredArchimedean, image_cast_int_Iio, NormedAddCommGroup.summable_imp_tendsto_of_complete, Real.tendsto_logb_nat_add_one_sub_logb, SSet.skeleton_zero, monotone_nat_of_le_succ, ProbabilityTheory.Kernel.stronglyAdapted_densityProcess, Urysohns.CU.tendsto_approx_atTop, tendsto_natCast_atTop_cobounded
|