ENat 📖 | CompOp | 1638 mathmath: ContinuousMap.dense_setOf_contDiff, TangentBundle.continuousLinearMapAt_model_space, Function.Embedding.encard_le, Order.coheight_add_one_le, Matroid.eRk_lt_top_iff, Dynamics.netMaxcard_monotone_subset, ENat.add_lt_top, Cardinal.ofENat_top, instContMDiffAddOfNatWithTopENatOfContinuousAdd, Cardinal.natCast_lt_toENat_iff, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, ENat.toENNReal_lt_top, AlgebraicGeometry.Scheme.height_of_isClosed, Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ, emultiplicity_le_emultiplicity_of_dvd_left, instLieAddGroupOfNatWithTopENat, SimpleGraph.ediam_le_iff, SimpleGraph.ediam_anti, IsDiscreteValuationRing.addVal_zero, Module.length_compositionSeries, Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity, Order.LTSeries.length_le_krullDim, SmoothBumpCovering.toSmoothPartitionOfUnity_eq_mul_prod, ENat.floor_pos, LeftInvariantDerivation.lift_zero, exists_contMDiffMap_zero_one_of_isClosed, SimpleGraph.vertexCoverNum_le_card_sub_one, ENat.top_pos, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, Ideal.height_le_spanFinrank, Order.krullDim_le_of_strictComono_and_surj, Matroid.eRk_loops, MvPowerSeries.weightedOrder_monomial, Topology.RelCWComplex.skeleton_top, AnalyticOn.exists_hasFTaylorSeriesUpToOn, instIsManifoldRealEuclideanSpaceFinModelWithCornersSelfTopWithTopENatElemHAddNatOfNatSphere, LeftInvariantDerivation.leibniz, ENat.lt_add_one_iff', smooth_barycentric_coord, ringKrullDim_succ_le_ringKrullDim_polynomial, Order.krullDim_of_noMaxOrder, Metric.externalCoveringNumber_eq_zero, Set.encard_eq_zero, Set.toENat_cardinalMk_subtype, PartENat.ofENat_le, ENat.self_le_mul_left, instIsContMDiffRiemannianBundleOfNatWithTopENat_1, emultiplicity_of_isUnit_right, Cardinal.toENat_eq_natCast_iff, ENat.card_le_card_of_injective, Matroid.eRk_lt_encard_iff_dep, PartENat.withTopEquiv_symm_apply, Metric.packingNumber_eq_zero, PowerSeries.le_order_subst_left', Order.krullDim_lt_coe_iff, ContDiffMapSupportedInClass.map_contDiff, ENat.toNat_one, ContDiffMapSupportedIn.norm_iteratedFDeriv_apply_le_seminorm, ENat.ceil_eq_top, Cardinal.ofENat_lt_ofNat, OpenPartialHomeomorph.contDiff_unitBallBall_symm, CategoryTheory.Retract.injectiveDimension_le, Set.encard_diff_add_encard, Ideal.height_le_iff_exists_minimalPrimes, Matroid.eRk_empty, ENat.coe_one, SimpleGraph.le_chromaticNumber_iff_colorable, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, smoothSheafCommRing.nonunits_stalk, ENat.card_prod, Ideal.height_of_subsingleton, Set.encard_union_eq, ContDiffMapSupportedIn.iteratedFDerivLM_apply, SimpleGraph.le_chromaticNumber_iff_coloring, ENat.iInf_mul_of_ne, Set.encard_prod, Matroid.eRank_loopyOn, Set.tsub_encard_le_encard_diff, Matrix.eRank_le_card_width, ENat.smul_sSup, SimpleGraph.eccent_bot, AddCircle.card_torsion_le_of_isSMulRegular, CategoryTheory.injectiveDimension_le_iff, ENat.card_lt_top, MvPowerSeries.le_order_mul, LinearMap.IsSymmetric.diagonalization_apply_self_apply, PartENat.ofENat_one, Cardinal.ofENat_le_ofNat, ContDiffBumpBase.smooth, Module.supportDim_eq_bot_iff_subsingleton, Cardinal.toENat_ofENat, Set.ncard_le_encard, ContinuousLinearEquiv.symm_toDiffeomorph, ContDiffMapSupportedIn.structureMapCLM_apply, SimpleGraph.chromaticNumber_pos, Matroid.eRk_singleton_le, LeftInvariantDerivation.coe_derivation, Order.krullDim_nonneg_iff, Dynamics.coverMincard_eq_zero_iff, Matroid.eRk_mono, Ideal.height_top, SmoothPartitionOfUnity.locallyFinite, ENat.ceil_add_ofNat, Ring.krullDimLE_iff, exists_smooth_one_nhds_of_subset_interior, ringKrullDim_eq_one_iff_of_isLocalRing_isDomain, SimpleGraph.diam_eq_zero_iff_ediam_eq_top, ENat.gc_toENNReal_floor, contMDiff_addInvariantVectorField, Cardinal.one_eq_ofENat, Module.length_of_free, untopD_coe_enat, SmoothPartitionOfUnity.nonneg, ENat.ceil_top, PowerSeries.order_expand, LeftInvariantDerivation.left_invariant', ENat.iSup_zero, Matrix.eRank_le_card_height, emultiplicity_add_eq_min, Cardinal.range_ofENat, Module.End.independent_genEigenspace, ENat.card_pos, Ideal.height_lt_top, Continuous.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, PartENat.toWithTop_natCast, ENat.toENNReal_strictMono, ENat.ceil_le_ceil, SmoothBumpCovering.exists_immersion_euclidean, IsOpen.exists_msmooth_support_eq, Order.length_le_coheight, Dynamics.netMaxcard_le_coverMincard, Order.height_add_one_le, Finset.set_encard_biUnion_le, LeftInvariantDerivation.left_invariant, IsOpen.exists_smooth_support_eq, Cardinal.toENatAux_eq_top, SmoothPartitionOfUnity.locallyFinite', ENat.one_lt_card_iff_nontrivial, Ideal.exists_finset_card_eq_height_of_isNoetherianRing, ENat.map_one, Set.encard_preimage_val_le_encard_left, Dynamics.coverMincard_finite_of_isCompact_invariant, SimpleGraph.Walk.edist_le, Set.encard_pair, Matroid.eRank_le_encard_add_eRk_compl, ENat.floor_add_ofNat, ENat.canLift, instLieGroupOfNatWithTopENatOfIsTopologicalGroup, Module.length_eq_zero, Finset.emultiplicity_prod, PartENat.withTopEquiv_one, Mathlib.Tactic.ENatToNat.coe_sub, ENat.iInf_toNat, smoothSheafCommRing.eval_germ, contMDiff_mulInvariantVectorField, ContinuousLinearEquiv.coe_toDiffeomorph_symm, Order.krullDim_pos_iff, ENat.coe_top_add_one, Order.krullDim_le_one_iff, SimpleGraph.ediam_eq_top, SimpleGraph.vertexCoverNum_le_iff, emultiplicity_zero_eq_zero_of_ne_zero, Module.supportDim_add_length_eq_supportDim_of_isRegular, contDiffOn_iff_continuousOn_differentiableOn, Dynamics.coverMincard_image_le, Set.chainHeight_le_encard, instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀, Dynamics.coverMincard_univ, contDiff_one_iff_fderiv, Ideal.sup_primeHeight_eq_ringKrullDim, contMDiff_equivTangentBundleProd_symm, SimpleGraph.eccent_eq_top_of_not_connected, Order.height_nat, Module.End.genEigenspace_directed, lt_emultiplicity_of_lt_multiplicity, ENat.monotone_map_iff, contDiff_zero, ContDiffMapSupportedIn.contDiff, Submodule.spanRank_toENat_eq_iInf_encard, Matroid.le_eRk_iff, Real.contDiffAt_rpow_const_of_le, ENat.ceil_add_natCast, Ideal.primeHeight_mono, Topology.RelCWComplex.coe_skeletonLT, smoothSheafCommRing.instLocalRing_stalk, ENat.le_floor, SimpleGraph.radius_eq_zero_iff, Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown, Module.End.maxGenEigenspace_eq, Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top, LinearMap.IsSymmetric.directSum_decompose_apply, Homeomorph.contDiff_unitBall, AddMonoid.minOrder_le_addOrderOf, Nat.count_le_setENCard, MvPowerSeries.le_weightedOrder_mul, emultiplicity_of_one_right, SimpleGraph.two_le_chromaticNumber_of_adj, Order.height_pos, contMDiff_infty, Topology.RelCWComplex.cellFrontier_subset_skeletonLT, Cardinal.toENat_eq_zero, SimpleGraph.card_le_chromaticNumber_iff_forall_surjective, Subgroup.IsComplement.encard_left, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, IsManifold.instLEInftyOfNatWithTopENat_2, SimpleGraph.exists_egirth_eq_length, MvPowerSeries.le_order_prod, ContDiffMapSupportedIn.contDiff', Topology.CWComplex.iUnion_openCell_eq_skeletonLT, Order.krullDim_eq_zero_of_unique, emultiplicity_lt_iff_not_dvd, ENat.floor_add_one, Order.le_krullDim_iff, Cardinal.toENat_eq_ofNat, exists_smooth_tsupport_subset, SimpleGraph.three_le_egirth, Dynamics.IsDynNetIn.card_le_netMaxcard, emultiplicity_le_emultiplicity_of_dvd_right, Cardinal.ofENat_eq_ofNat, SimpleGraph.chromaticNumber_cycleGraph_of_even, Stream'.Seq.length'_of_terminates, Module.End.maxGenEigenspace_eq_genEigenspace_finrank, emultiplicity_pos_of_dvd, Ideal.primeHeight_lt_top, Module.End.mapsTo_genEigenspace_of_comm, MeasureTheory.MemLp.exist_eLpNorm_sub_le, ENat.card_eq_zero_iff_empty, Dynamics.coverMincard_empty, PowerSeries.order_mul_ge, Nat.Prime.emultiplicity_factorial, SimpleGraph.chromaticNumber_le_sum_right, Dynamics.netMaxcard_infinite_iff, ENat.sub_ne_top_iff, contDiffOn_of_continuousOn_differentiableOn, Set.encard_union_add_encard_inter, ENat.floor_add_natCast, ENat.forall_natCast_le_iff_le, WithBot.lt_add_one_iff, Cardinal.ofENat_mono, analyticOrderAt_eq_top, contDiffWithinAt_nat, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, Set.encard_preimage_val_le_encard_right, ZMod.minOrder_of_prime, Metric.coveringNumber_two_mul_le_externalCoveringNumber, PowerSeries.le_order_smul, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, Matroid.IsNonloop.eRk_eq, ENat.mul_iSup, ENat.sSup_eq_zero, Ideal.height_strict_mono_of_is_prime, PowerSeries.order_finite_iff_ne_zero, Matroid.eRank_eq_top, LeftInvariantDerivation.lift_add, Polynomial.le_trailingDegree_C, ContDiffMapSupportedIn.iteratedFDerivLM_eq_withOrder, SimpleGraph.chromaticNumber_mono_of_embedding, le_minSmoothness, ringKrullDim_succ_le_ringKrullDim_powerseries, Polynomial.trailingDegree_eq_zero, contDiffOn_infty, Polynomial.height_eq_height_add_one, OpenPartialHomeomorph.contDiff_univUnitBall, MvPowerSeries.le_weightedOrder_prod, ENat.floor_top, Nat.cast_analyticOrderNatAt, Dynamics.one_le_coverMincard_iff, ENat.map_natCast_eq_zero, tangentBundle_model_space_coe_chartAt, ENat.ceil_sub_one, ENat.toNat_zero, SimpleGraph.chromaticNumber_top, Dynamics.coverMincard_monotone_time, Order.krullDim_eq_top, contDiff_iff_forall_nat_le, LeftInvariantDerivation.lift_smul, Nat.Prime.emultiplicity_le_emultiplicity_choose_add, Order.coheight_le_krullDim, SmoothPartitionOfUnity.sum_finsupport', SimpleGraph.Colorable.chromaticNumber_eq_sInf, ENat.epow_natCast, contDiff_succ_iff_fderiv, TestFunction.contDiff, contMDiffAt_mulInvariantVectorField, Ideal.exists_ltSeries_length_eq_height, MvPowerSeries.weightedOrder_monomial_of_ne_zero, ENat.map_natCast_strictMono, Matroid.eRk_lt_encard_iff_dep_of_finite, IsContDiffImplicitAt.one_le, Order.krullDim_nonpos_iff_forall_isMax, instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup, ZMod.minOrder, SimpleGraph.edist_eq_top_of_not_reachable, ENat.biSup_add', SimpleGraph.chromaticNumber_le_of_forall_imp, Ideal.primeHeight_eq_ringKrullDim_iff, FiniteMultiplicity.emultiplicity_self, FiniteMultiplicity.emultiplicity_eq_multiplicity, MvPowerSeries.weightedOrder_mul, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, PowerSeries.le_order_subst_right', Topology.RelCWComplex.iUnion_openCell_eq_skeleton, Dynamics.netMaxcard_zero, MvPowerSeries.le_weightedOrder_map, Module.length_eq_zero_of_subsingleton_ring, le_emultiplicity_map, ENat.iInf_mul', Nat.two_pow_sub_pow, Stream'.Seq.length'_le_iff, ringKrullDim_nonneg_of_nontrivial, ENat.add_right_injective_of_ne_top, mdifferentiableAt_addInvariantVectorField, ringKrullDimZero_iff_ringKrullDim_eq_zero, Cardinal.toENatAux_eq_nat, Matroid.eRk_dual_add_eRank', ContDiffMapSupportedIn.seminorm_le_iff, Cardinal.ofENat_lt_aleph0, MvPowerSeries.nat_le_order, Nat.Prime.emultiplicity_factorial_mul, ENat.ne_top_iff_exists, ENat.one_le_card_iff_nonempty, AddHom.ENatMap_apply, Submodule.length_lt, contDiffAt_one_iff, hasFTaylorSeriesUpTo_zero_iff, Order.coheight_eq_coe_add_one_iff, Order.krullDim_nonpos_iff_forall_isMin, Module.length_pos_iff, SimpleGraph.vertexCoverNum_le_vertexCoverNum_of_injective, LeftInvariantDerivation.comp_L, IsOpen.exists_contMDiff_support_eq_aux, Subgroup.IsComplement.encard_right, ENat.map_top, ENat.measurable_iff, Mathlib.Tactic.ENatToNat.not_lt_top, ENat.top_epow, SimpleGraph.edist_self, Monoid.minOrder_le_natCard, Mathlib.Tactic.ENatToNat.coe_mul, Matroid.eRank_eq_top_iff, AddMonoid.le_minOrder, ENat.card_le_one_iff_subsingleton, Cardinal.toENat_lt_natCast_iff, ENat.mem_nhds_iff, Module.supportDim_le_of_injective, instIsManifoldRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, SmoothBumpCovering.toSmoothPartitionOfUnity_apply, Polynomial.le_trailingDegree_monomial, Function.hasTemperateGrowth_iff_isBigO, Metric.externalCoveringNumber_le_one_of_ediam_le, minSmoothness_eq_infty, ENat.zero_epow, Order.krullDim_int, Set.Finite.encard_lt_top, SimpleGraph.eccent_le_one_iff, Metric.coveringNumber_empty, PartENat.toWithTop_lt, ENat.card_lt_top_of_finite, ENat.lift_one, Submodule.inf_genEigenspace, Cardinal.toENatAux_nat, Matroid.eRk_le_eRk_add_eRk_diff, ENat.floor_le_ceil, Dynamics.coverMincard_closure_le, contDiff_all_iff_nat, Real.smoothTransition.contDiffAt, MvPowerSeries.nat_le_weightedOrder, Set.encard_union_le, contDiffOn_succ_of_fderivWithin, Metric.externalCoveringNumber_empty, multiplicity_addValuation_apply, Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex, Set.encard_strictMono, Polynomial.trailingDegree_le_trailingDegree, Submodule.height_strictMono, ContDiffBump.contDiff, IsPrincipalIdealRing.height_eq_one_of_isMaximal, Cardinal.nat_eq_ofENat, emultiplicity_pow_prime_pow_sub_pow_prime_pow, Matroid.eRank_emptyOn, ENat.epow_mul, Cardinal.toENat_lift, Module.End.map_genEigenrange_le, Matroid.eRk_compl_insert_union_add_eRk_compl_insert_inter_le, Set.encard_iUnion_of_finite, Set.coe_fintypeCard, ENat.add_one_le_iff, Int.emultiplicity_pow_sub_pow, Polynomial.trailingDegree_C_mul_X_pow, Stream'.Seq.length'_cons, SimpleGraph.edist_top, ENat.iInf_coe_lt_top, ENat.instOrderTopology, contDiffOn_omega_iff_analyticOn, ENat.ceil_lt_top, MvPowerSeries.one_le_order_iff_constCoeff_eq_zero, SimpleGraph.vertexCoverNum_top, Metric.externalCoveringNumber_anti, ENat.toENNReal_sub, mdifferentiable_mulInvariantVectorField, Nat.emultiplicity_pow_add_pow, SimpleGraph.chromaticNumber_eq_zero_of_isEmpty, Order.height_le_krullDim, ENat.iInf_mul, Cardinal.toENat_le_ofNat, Matroid.eRk_insert_le_add_one, Set.chainHeight_mono, Metric.exists_smooth_forall_closedBall_subset, contDiffWithinAt_zero, Ideal.height_le_height_add_of_liesOver, instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle, FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq, Polynomial.trailingDegree_zero, Cardinal.instCanLiftENatOfENatLeAleph0, ENat.epow_add, contDiffOn_infty_iff_fderivWithin, MvPowerSeries.le_order_subst, MvPowerSeries.le_weightedOrder_pow, analyticOrderAt_centeredMonomial, ENat.add_iSup, le_emultiplicity_of_le_multiplicity, Module.End.hasUnifEigenvalue_iff_mem_spectrum, contMDiff_zero_iff, CategoryTheory.injectiveDimension_ge_iff, LeftInvariantDerivation.evalAt_coe, contDiffOn_nat_iff_continuousOn_differentiableOn, Ideal.height_le_height_add_one_of_mem, PowerSeries.le_order_map, Matroid.spanning_iff_eRk_le', SimpleGraph.chromaticNumber_eq_iInf, SimpleGraph.eccent_eq_zero_iff, ENat.mul_sSup, Metric.packingNumber_two_mul_le_externalCoveringNumber, emultiplicity_le_emultiplicity_iff, PartENat.toWithTop_zero', SimpleGraph.chromaticNumber_sum, Set.encard_empty, Stream'.Seq.drop_length', Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, MvPowerSeries.min_weightedOrder_le_add, Module.End.Eigenvalues.mk_val, Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt, Set.encard_eq_top_iff, Module.coe_length, Topology.RelCWComplex.cellFrontier_subset_skeleton, ENat.toENNReal_top, SmoothPartitionOfUnity.le_one, Order.bot_lt_krullDim, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, ENat.eq_top_iff_forall_gt, ENat.nhds_eq_pure, topologicalKrullDim_subspace_le, LinearMap.finrank_genEigenspace_le, LinearMap.IsSymmetric.diagonalization_symm_apply, Continuous.exists_contMDiff_approx, Dynamics.coverMincard_finite_of_isCompact_uniformContinuous, ContinuousMultilinearMap.hasFTaylorSeriesUpTo_iteratedFDeriv, Ideal.height_le_card_of_mem_minimalPrimes_span, SimpleGraph.chromaticNumber_le_card, exists_contMDiffMap_zero_one_nhds_of_isClosed, PointedContMDiffMap.smul_def, topologicalKrullDim_zero_of_discreteTopology, ringKrullDim_quotient_le, Module.End.iSup_genEigenspace_eq, Matroid.eRk_inter_add_eRk_union_le, SimpleGraph.chromaticNumber_eq_two_iff, ENat.map_eq_top_iff, Set.encard_eq_three, Order.krullDim_eq_iSup_coheight_of_nonempty, Module.End.genEigenspace_inf_le_add, smoothSheafCommRing.isUnit_stalk_iff, contMDiff_vectorSpace_iff_contDiff, Nat.Prime.emultiplicity_choose', ENat.coe_sSup, ENat.coe_toNat_le_self, Module.End.eigenspace_le_genEigenspace, ringKrullDim_succ_le_of_surjective, contDiff_bernoulliFun, PartENat.withTopEquiv_ofNat, contDiff_iff_iteratedDeriv, LeftInvariantDerivation.map_zero, AddSubgroup.IsComplement.encard_right, EuclideanSpace.instIsManifoldSphere, AddSubgroup.IsComplement.encard_left, PowerSeries.order_monomial, ENat.sInf_eq_zero, ENat.top_sub_one, Ideal.exists_isMaximal_height, SimpleGraph.vertexCoverNum_mono, IsDiscreteValuationRing.addVal_def', ENat.instContinuousMul, emultiplicity_eq_zero_iff_multiplicity_eq_zero, Ideal.primeHeight_le_ringKrullDim, Order.krullDim_eq_iSup_length, ringKrullDim_eq_bot_of_subsingleton, TangentBundle.coordChange_model_space, Dynamics.netMaxcard_empty, Dynamics.IsDynCoverOf.coverMincard_le_card, Matroid.eRk_dual_add_eRank, Metric.externalCoveringNumber_mono_set, Stream'.Seq.length'_nil, Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim, Cardinal.one_le_ofENat, contDiffOn_abs, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, fdifferential_apply, Metric.IsCover.externalCoveringNumber_le_encard, Order.coheight_pos_of_lt_top, instContMDiffInv₀OfNatWithTopENat, CategoryTheory.projectiveDimension_lt_iff, Module.length_eq_top_iff_infiniteDimensionalOrder, SmoothBumpFunction.contMDiffAt, Metric.coveringNumber_eq_one_of_ediam_le, RingHom.ENatMap_apply, Irreducible.addVal_pow, SimpleGraph.egirth_eq_top, Order.coheight_eq_coe_iff_maximal_le_coheight, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, ENat.ceil_le, ENat.epow_right_mono, SimpleGraph.chromaticNumber_le_iff_colorable, Ideal.primeHeight_strict_mono, Set.encard_diff_add_encard_of_subset, SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable, hasFTaylorSeriesUpToOn_zero_iff, Topology.RelCWComplex.openCell_subset_skeletonLT, ENat.toNat_eq_iff, Order.height_pos_of_bot_lt, Set.encard_eq_top, Order.IsMax.coheight_eq_zero, Topology.RelCWComplex.closedCell_subset_skeletonLT, PowerSeries.le_order_mul, SmoothBumpCovering.sum_toSmoothPartitionOfUnity_eq, Set.Nat.encard_range, ENat.ceil_lt, Set.encard_lt_top_iff, smoothSheafCommRing.evalHom_germ, ENat.instContinuousAdd, SimpleGraph.edist_pos_of_ne, ENat.coe_toNat, L_mul, LeftInvariantDerivation.coe_sub, emultiplicity_pow_self, Set.encard_le_card, ringKrullDim_le_iff_height_le, MvPowerSeries.ne_zero_iff_weightedOrder_finite, contDiffOn_succ_iff_fderiv_of_isOpen, contDiff_iff_continuous_differentiable, SimpleGraph.chromaticNumber_eq_card_iff, Set.Finite.encard_lt_encard, natCast_le_analyticOrderAt, Dynamics.coverMincard_antitone, SimpleGraph.egirth_bot, Cardinal.ofENat_eq_zero, ENat.ceil_pos, ENat.map_natCast_mul, ENat.card_eq_top, hasFTaylorSeriesUpToOn_succ_iff_right, emultiplicity_eq_zero, Dynamics.netMaxcard_antitone, SimpleGraph.vertexCoverNum_le_encard_edgeSet, LeftInvariantDerivation.left_invariant'', Order.krullDim_nonpos_of_subsingleton, Matroid.IsRkFinite.eRk_lt_top, Order.height_eq_zero, Matroid.Indep.encard_le_eRk_of_subset, PartENat.toWithTop_add, IsDiscreteValuationRing.addVal_uniformizer, contDiff_nat_iff_iteratedDeriv, Matroid.eRank_le_encard_ground, Order.coheight_eq_iSup_head_eq, Cardinal.ofENat_add, ENat.sub_eq_top_iff, ExistsContDiffBumpBase.u_exists, ENat.coe_mul, instIsManifoldMinSmoothnessOfNatWithTopENat_1, ENat.ceil_add_le, SimpleGraph.vertexCoverNum_lt_card, ENat.lt_ceil, AnalyticAt.analyticOrderAt_deriv_add_one, Nat.Prime.emultiplicity_choose, Matroid.eRank_lt_top_iff, Int.two_pow_two_pow_add_two_pow_two_pow, ENat.coe_iSup, ENat.smul_iSup, Order.krullDim_WithTop, PartENat.toWithTop_le, contDiff_of_differentiable_iteratedFDeriv, IsInducing.topologicalKrullDim_le, contDiffPointwiseHolderAt_iff, ENat.top_epow_top, emultiplicity_eq_top, SmoothPartitionOfUnity.sum_eq_one', Matroid.eRk_insert_inter_add_eRk_insert_union_le, Ideal.height_mono, Order.height_of_noMinOrder, Submodule.spanFinrank_span_le_encard, ringKrullDim_le_ringKrullDim_quotient_add_card, Dynamics.coverMincard_zero, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, Matroid.Indep.encard_le_eRank, ENat.continuousAt_sub, ENat.natCast_lt_succ, Order.krullDim_eq_iSup_height_of_nonempty, SmoothPartitionOfUnity.mem_finsupport, PowerSeries.order_zero, PowerSeries.one_le_order_iff_constCoeff_eq_zero, Metric.IsCover.coveringNumber_le_encard, PartENat.withTopEquiv_symm_ofNat, IsOpen.exists_contMDiff_support_eq, emultiplicity_zero, Ideal.height_le_ringKrullDim_quotient_add_one, measurable_encard, ENat.toENNRealOrderEmbedding_apply, Order.coheight_int, ENat.sub_iSup, ENat.iInf_eq_top_of_isEmpty, Nat.emultiplicity_two_factorial_lt, Real.contDiff_fourierIntegral, ENat.toENNRealRingHom_apply, instContMDiffVectorBundleOfNatWithTopENat, contDiffWithinAt_omega_iff_analyticWithinAt, ENat.floor_lt_ceil, ENat.toENNReal_zero, smoothRightMul_one, contMDiff_smul, le_emultiplicity_of_pow_dvd, trivializationAt_model_space_apply, Real.contDiffAt_arcsin_iff, ENat.iInf_coe_eq_top, MvPowerSeries.le_weightedOrder_smul, Ideal.height_le_iff, contDiffOn_zero, SimpleGraph.chromaticNumber_le_two_iff_isBipartite, analyticOrderAt_mul, SimpleGraph.vertexCoverNum_eq_zero, ENat.floor_lt_top, SimpleGraph.CompleteBipartiteGraph.chromaticNumber, SimpleGraph.ediam_top, ENat.coe_toNatHom, Polynomial.le_trailingDegree_mul, ENat.map_natCast_injective, SimpleGraph.two_le_chromaticNumber_iff_ne_bot, ENat.ceil_natCast_add, hasFTaylorSeriesUpTo_succ_nat_iff_right, OpenPartialHomeomorph.contDiffOn_univUnitBall_symm, Order.coheight_coe_withTop, MvPowerSeries.le_weightedOrder_subst, Matrix.eRank_zero, Dynamics.coverMincard_union_le, ENat.gc_ceil_toENNReal, Cardinal.ofENat_injective, Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ, ENat.exists_eq_iInf, ENat.mul_top', MeasureTheory.stoppedProcess_eq, Stream'.Seq.at_least_as_long_as_coind, Order.coheight_of_noMaxOrder, hasFTaylorSeriesUpToOn_succ_nat_iff_right, Order.coheight_eq_krullDim_Ici, Module.End.disjoint_genEigenspace, Module.length_le_of_surjective, Cardinal.ofENat_eq_one, ENat.lift_zero, ENat.one_le_iff_ne_zero_withTop, LinearMap.IsSymmetric.orthogonalFamily_eigenspaces', Order.height_eq_iSup_lt_height, Order.height_eq_coe_add_one_iff, SimpleGraph.eccent_eq_one_iff, ENat.floor_sub_natCast, Submodule.inf_iSup_genEigenspace, ENat.floor_coe, IsClosedEmbedding.topologicalKrullDim_le, Polynomial.trailingDegree_le_of_ne_zero, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, PowerSeries.coe_toNat_order, FiniteMultiplicity.emultiplicity_le_of_multiplicity_le, contDiffOn_of_differentiableOn, Matroid.eRk_le_iff, Matroid.eRk_eq_top_iff, AnalyticAt.analyticOrderAt_eq_natCast, SimpleGraph.le_chromaticNumber_iff_forall_surjective, Cardinal.ofENat_mul, Order.krullDim_enat, Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, Order.height_le_coe_iff, Topology.RelCWComplex.iUnion_skeletonLT_eq_complex, PartENat.toWithTop_one, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, instIsContMDiffRiemannianBundleOfNatWithTopENat_2, Order.height_eq_coe_iff, Matroid.eRk_loopyOn, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', SmoothBumpCovering.embeddingPiTangent_injective_mfderiv, Topology.RelCWComplex.skeletonLT_zero_eq_base, SimpleGraph.ediam_eq_one, Cardinal.ofENat_le_ofENat, ENat.toENNReal_lt, AddMonoidHom.ENatMap_apply, ENat.floor_one, Polynomial.le_trailingDegree_C_mul_X_pow, SimpleGraph.edist_le_eccent, Cardinal.ofNat_lt_ofENat, SimpleGraph.Colorable.chromaticNumber_le, SimpleGraph.edist_triangle, exists_msmooth_support_eq_eq_one_iff, Matrix.eRank_subsingleton, ENat.ceil_sub_natCast, ENat.coe_iInf, tangentBundle_model_space_coe_chartAt_symm, Matroid.IsLoop.eRk_eq, SmoothPartitionOfUnity.coe_finsupport, tangentBundleModelSpaceHomeomorph_coe, Order.height_eq_krullDim_Iic, Emetric.exists_contMDiffMap_forall_closedBall_subset, MvPowerSeries.weightedOrder_mul_ge, SchwartzMap.contDiffAt, MvPowerSeries.le_order, contDiffOn_infty_iff_fderiv_of_isOpen, ENat.card_sum, Module.length_bot, ENat.ceil_zero, Set.one_le_encard_insert, IsManifold.instLEInftyOfNatWithTopENat_1, Set.Nonempty.encard_pos, PowerSeries.le_order_pow_of_constantCoeff_eq_zero, ENat.toNatHom_apply, R_mul, Order.length_le_height, ENat.mul_iInf_of_ne, MvPowerSeries.order_le, ENat.toENNReal_min, SimpleGraph.IsVertexCover.vertexCoverNum_le, Nat.Prime.emultiplicity_self, Module.End.mem_genEigenspace_top, smoothLeftMul_one, Module.End.injOn_genEigenspace, emultiplicity_one_left, IsDiscreteValuationRing.addVal_mul, IsDiscreteValuationRing.addVal_add, ENat.mul_epow, tangentBundleCore_coordChange_model_space, Module.length_eq_one, Metric.exists_contMDiffMap_forall_closedBall_subset, Metric.externalCoveringNumber_eq_one_of_ediam_le, Stream'.Seq.length'_of_not_terminates, ENat.epow_one, ENat.ceil_add_toENNReal, Order.height_le_height_apply_of_strictMono, Module.End.genEigenspace_one, exists_msmooth_zero_iff_one_iff_of_isClosed, LeftInvariantDerivation.map_add, Set.encard_iUnion_le_of_finite, AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top, contDiffOn_all_iff_nat, ENat.coe_toNat_eq_self, ENat.card_eq_top_of_infinite, instIsManifoldMinSmoothnessOfNatWithTopENat, Nat.Prime.emultiplicity_choose_prime_pow, contDiffGroupoid_zero_eq, ENat.LEInfty.out, smoothSheaf.obj_eq, ringKrullDim_add_length_eq_ringKrullDim_of_isRegular, SmoothPartitionOfUnity.finsum_smul_mem_convex, SimpleGraph.edist_bot, Order.krullDim_le_one_iff_of_boundedOrder, SubMulAction.ENat_card_ofStabilizer_add_one_eq, contDiffOn_succ_iff_deriv_of_isOpen, Int.two_pow_sub_pow', LeftInvariantDerivation.coe_add, Matroid.eRk_union_le_eRk_add_eRk, Matroid.eRk_le_eRk_inter_add_eRk_diff, Cardinal.toENatAux_gc, AddCircle.card_torsion_le_of_isSMulRegular_int, instContMDiffMulOfNatWithTopENat, Cardinal.toNat_toENat, ENat.iSup_natCast, SmoothPartitionOfUnity.sum_le_one', SimpleGraph.ediam_eq_zero_of_subsingleton, Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton, IsLocalization.AtPrime.ringKrullDim_eq_height, SmoothBumpCovering.embeddingPiTangent_ker_mfderiv, SmoothPartitionOfUnity.sum_nonneg, Manifold.riemannianEDist_def, Metric.coveringNumber_pos_iff, Polynomial.trailingDegree_C, ENat.toENNReal_mono, ENat.coe_inj, ENat.floor_mono, Ideal.height_le_ringKrullDim_quotient_add_encard, PointedContMDiffMap.instIsScalarTowerSomeENatTop, Ideal.primeHeight_add_one_le_of_lt, Set.one_le_chainHeight_iff, tangentBundleCore.isContMDiff, pow_dvd_iff_le_emultiplicity, ENat.epow_left_mono, SimpleGraph.cliqueNum_le_chromaticNumber, ENat.floor_sub_toENNReal, Polynomial.natTrailingDegree_le_trailingDegree, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors, contDiffOn_iff_forall_nat_le, contDiff_succ_iff_fderiv_apply, ENat.add_one_eq_coe_top_iff, ENat.le_ceil, OpenPartialHomeomorph.contDiff_univBall, Order.krullDim_eq_iSup_coheight, PartENat.toWithTop_natCast', emultiplicity_geom_sum₂_eq_one, Order.krullDim_eq_bot_iff, PowerSeries.min_order_le_order_add, TangentBundle.contMDiffVectorBundle, PowerSeries.order_exp, Set.encard_eq_coe_toFinset_card, fdifferential_comp, Module.supportDim_quotSMulTop_succ_eq_supportDim, Matroid.IsCircuit.eRk_add_one_eq, SimpleGraph.ediam_le_two_mul_radius, Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT, LeftInvariantDerivation.coe_injective, Order.coheight_eq_zero, Cardinal.ofENat_eq_nat, SimpleGraph.edist_eq_sInf, PartENat.withTopEquiv_symm_one, contDiffAt_succ_iff_hasFDerivAt, ENat.top_sub_coe, toENat_rank_span_set, ENat.epow_eq_one_iff, ENat.iSup_mul, PartENat.withTopEquiv_natCast, SmoothBumpCovering.exists_finset_toSmoothPartitionOfUnity_eventuallyEq, contDiffOn_tsum_cexp, ExistsContDiffBumpBase.u_smooth, Set.encard_mono, dvd_iff_emultiplicity_pos, VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral', Real.contDiff_fourier, ENat.add_lt_add_iff_left, Set.encard_singleton_inter, LeftInvariantDerivation.coe_neg, Dynamics.coverMincard_le_pow, Ideal.height_le_iff_covBy, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, ENat.isOpen_singleton, SimpleGraph.eccent_le_ediam, Dynamics.coverMincard_mul_le_pow, Set.Infinite.encard_eq, le_analyticOrderAt_sub, Order.coheight_top, contDiffWithinAt_infty, SimpleGraph.chromaticNumber_cycleGraph_of_odd, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson, le_analyticOrderAt_add, tangentBundle_model_space_chartAt, Set.chainHeight_empty, ENat.epow_eq_zero_iff, Dynamics.netMaxcard_monotone_time, ENat.coe_sub, Module.length_eq_one_iff, ENat.one_le_epow, PartENat.toWithTop_top, SimpleGraph.ediam_eq_iSup_iSup_edist, Matroid.eRank_eq_zero_iff, Stream'.Seq.length'_eq_zero_iff_nil, contMDiffAt_iff_nat, Cardinal.toENat_strictMonoOn, LinearMap.IsSymmetric.direct_sum_isInternal, Order.krullDim_eq_iSup_height, Matroid.eRk_eq_one_iff, AddMonoid.le_minOrder_iff_forall_addSubgroup, Order.coheight_eq_top_iff, ENat.toNat_mul, Metric.externalCoveringNumber_singleton, SimpleGraph.eccent_pos_iff, cot_pi_mul_contDiffWithinAt, IsOpen.exists_msmooth_support_eq_aux, IsPrincipalIdealRing.ringKrullDim_eq_one, Real.contDiffAt_rpow_const, SimpleGraph.vertexCoverNum_of_subsingleton, ContMDiffMap.mdifferentiable, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, Matroid.ExchangeProperty.encard_diff_le_aux, OpenPartialHomeomorph.contDiff_unitBallBall, Order.height_top_eq_krullDim, exists_contMDiff_zero_iff_one_iff_of_isClosed, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, SimpleGraph.Connected.exists_walk_length_eq_edist, Order.coheight_le_coheight_apply_of_strictMono, Cardinal.ofNat_le_ofENat, IsDiscreteValuationRing.addVal_pow, Order.krullDim_eq_zero_iff_of_orderTop, VectorFourier.contDiff_fourierIntegral, Module.length_pos, ENat.addLECancellable_coe, PartENat.withTopEquiv_top, Submodule.spanRank_toENat_eq_iInf_finset_card, ContDiffBump.contDiff_normed, ENat.ceil_sub_toENNReal, SimpleGraph.edist_anti, Diffeology.isPlot_iff_contDiff, PartENat.toWithTop_top', ENat.pow_lt_top_iff, Module.length_finsupp, Set.encard_le_coe_iff_finite_ncard_le, ENat.coe_sInf, PartENat.toWithTop_zero, MvPowerSeries.le_order_smul, LeftInvariantDerivation.map_smul, Mathlib.Tactic.ENatToNat.coe_zero, MvPowerSeries.order_eq_top_iff, ENat.toENNReal_eq_top, ringKrullDim_eq_zero_of_isField, PartENat.ofENat_lt, PowerSeries.le_order_pow, Order.height_bot, analyticOrderAt_pow, Order.one_le_krullDim_iff, emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso, ENat.iSup_eq_zero, squarefree_iff_emultiplicity_le_one, ENat.eq_top_iff_forall_ne, contDiff_iff_ftaylorSeries, SmoothPartitionOfUnity.sum_eq_one, Set.encard_eq_one, Metric.coveringNumber_subset_le, ENat.toENNReal_one, Order.coheight_le_iff', Matroid.eRk_eq_zero_iff', Order.krullDim_le_of_strictMono, Cardinal.continuum_toENat, ContDiffBump.contDiffAt, ENat.mem_nhds_natCast_iff, ringKrullDim_le_iff_isMaximal_height_le, ringKrullDim_le_ringKrullDim_add_card, ENat.recTopCoe_coe, smoothSheaf.eval_germ, analyticOrderAt_id, Set.encard_eq_add_one_iff, Polynomial.trailingDegree_lt_wf, PowerSeries.order_pow, CategoryTheory.projectiveDimension_le_iff, MvPowerSeries.weightedOrder_eq_nat, SmoothBumpCovering.embeddingPiTangent_injOn, ENat.recTopCoe_zero, SimpleGraph.chromaticNumber_le_one_of_subsingleton, ENat.toENNReal_add, Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT, Metric.coveringNumber_le_packingNumber, Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, contMDiffAt_vectorSpace_iff_contDiffAt, ENat.le_coe_iff, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, PartENat.withTopEquiv_le, Monoid.le_minOrder_iff_forall_subgroup, Mathlib.Tactic.ENatToNat.coe_ofNat, MvPowerSeries.order_expand, Module.supportDim_le_ringKrullDim, PointedContMDiffMap.instIsScalarTowerSomeENatTopContMDiffMapModelWithCornersSelf, LeftInvariantDerivation.coe_smul, Ideal.primeHeight_eq_zero_iff, Set.encard_le_encard_iff_encard_diff_le_encard_diff, Module.length_le_of_injective, ENat.recTopCoe_one, ENat.iSup_add, ENat.nhds_natCast, PartENat.withTopEquiv_lt, ENat.floor_zero, Set.encard_ne_add_one, PartENat.withTopEquiv_apply, Module.supportDim_le_supportDim_quotSMulTop_succ, CategoryTheory.projectiveDimension_ge_iff, Module.End.genEigenspace_zero_nat, emultiplicity_of_unit_right, mdifferentiable_addInvariantVectorField, FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt, Matroid.eRk_le_eRank, ENat.lt_add_one_iff, ENat.addLECancellable_of_ne_top, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, L_apply, Module.length_prod, Cardinal.ofENat_lt_ofENat, SimpleGraph.ediam_eq_zero_iff_subsingleton, IsDiscreteValuationRing.addVal_eq_zero_iff, AnalyticAt.analyticOrderAt_comp, expNegInvGlue.contDiff, Matroid.eRank_add_eRank_dual, Int.emultiplicity_pow_add_pow, SimpleGraph.le_chromaticNumber_of_pairwise_adj, AnalyticOnNhd.isClopen_setOf_analyticOrderAt_eq_top, contDiffAt_infty, Module.End.genEigenspace_top, Matroid.eRk_eq_zero_iff, TangentBundle.symmL_model_space, PowerSeries.le_order_subst, ENat.pow_eq_top_iff, ringKrullDim_lt_top, Diffeology.IsContDiffCompatible.isPlot_iff, Cardinal.ofENat_nat, CategoryTheory.injectiveDimension_lt_iff, SimpleGraph.chromaticNumber_mono, Topology.RelCWComplex.openCell_subset_skeleton, Cardinal.ofENat_strictMono, PartENat.toWithTop_some, Cardinal.toENatAux_zero, Module.End.genEigenrange_nat, ENat.ceil_mono, AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top, Polynomial.ringKrullDim_le, SimpleGraph.chromaticNumber_eq_zero_of_isempty, PowerSeries.order_prod, ENat.mul_iInf, Cardinal.toENat_le_iff_of_le_aleph0, PartENat.ofENat_coe, ENat.floor_eq_top, ENat.card_eq_coe_fintype_card, SmoothBumpCovering.comp_embeddingPiTangent_mfderiv, ENat.coe_lt_coe, SimpleGraph.diam_def, PowerSeries.order_le, ENat.sSup_mul, emultiplicity_lt_top, ENat.iSup_coe_eq_top, ENat.recTopCoe_top, MeasureTheory.LocallyIntegrable.exists_contDiff_dist_le_of_forall_mem_ball_dist_le, contDiff_nat_iff_continuous_differentiable, Cardinal.toENat_eq_top, contDiffOn_of_differentiableOn_deriv, differentiableWithinAt_localInvariantProp, Matroid.eRk_lt_encard_of_dep_of_finite, PowerSeries.order_zero_of_unit, ExistsContDiffBumpBase.y_smooth, ENat.coe_le_coe, MvPowerSeries.weightedOrder_le, Order.coheight_nat, SimpleGraph.ediam_eq_top_of_not_connected, contDiffWithinAt_iff_forall_nat_le, ENat.top_sub_ofNat, SimpleGraph.edist_le_ediam, ENat.add_one_pos, AddMonoid.minOrder_eq_top_iff, PowerSeries.order_one, Order.coheight_le_coe_iff, SmoothPartitionOfUnity.exists_pos_of_mem, SimpleGraph.eq_top_iff_forall_eccent_eq_one, IsManifold.instLEInftySomeENat, SimpleGraph.completeMultipartiteGraph.chromaticNumber, Cardinal.one_lt_ofENat, Topology.CWComplex.iUnion_openCell_eq_skeleton, ENat.ceil_one, Module.length_pi_of_fintype, exists_smooth_zero_one_of_isClosed, Ideal.map_height_le_one_of_mem_minimalPrimes, ENat.instDiscreteMeasurableSpace, CategoryTheory.projectiveDimension_eq_bot_iff, PartENat.withTopEquiv_symm_zero, Module.length_eq_zero_iff, Diffeology.IsPlot.contDiff, tangentBundleModelSpaceHomeomorph_coe_symm, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, Topology.RelCWComplex.skeleton_monotone, PartENat.toWithTop_one', Set.Finite.exists_encard_eq_coe, expNegInvGlue.contDiff_polynomial_eval_inv_mul, Dynamics.netMaxcard_finite_iff, Set.encard_eq_four, SmoothBumpCovering.embeddingPiTangent_injective, contDiff_one_iff_hasFDerivAt, Set.Finite.encard_eq_coe, instContMDiffVectorBundleOfNatWithTopENat_1, exists_contMDiff_support_eq_eq_one_iff, Diffeomorph.instContinuousMapClassSomeENatTop, Int.two_pow_sub_pow, Cardinal.ofENat_lt_nat, MeasureTheory.stoppedProcess_eq', Set.encard_image_le, Order.krullDim_le_one_iff_forall_isMax, MvPowerSeries.weightedOrder_add_of_weightedOrder_ne, IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim, Cardinal.toENatAux_eq_zero, Order.krullDim_withBot, Polynomial.trailingDegree_one, Matroid.eRk_union_le_encard_add_eRk, Module.End.generalized_eigenvec_disjoint_range_ker, ENat.floor_lt, LeftInvariantDerivation.map_sub, Cardinal.ofENat_le_one, Metric.packingNumber_singleton, contMDiff_equivTangentBundleProd, instIsManifoldOfNatWithTopENatOfMinSmoothness_1, ENat.ceil_sub_ofNat, SmoothPartitionOfUnity.sum_finsupport_smul_eq_finsum, Order.krullDim_pos_iff_of_orderTop, SubAddAction.ENat_card_ofStabilizer_add_zero_eq, Nat.Prime.emultiplicity_pow, LeftInvariantDerivation.map_neg, Cardinal.ofENat_pos, SimpleGraph.radius_le_ediam, contDiffOn_of_continuousOn_differentiableOn_deriv, Matroid.eRk_union_le_eRk_add_encard, IsDiscreteValuationRing.addVal_eq_top_iff, ENat.sub_top, ringKrullDim_nat, contDiff_omega_iff_analyticOnNhd, Module.length_eq_add_of_exact, ENat.add_le_add_iff_right, Set.encard_coe_eq_coe_finsetCard, Nat.Prime.emultiplicity_factorial_le_div_pred, UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors, ENat.toENNReal_mul, Cardinal.toENat_le_natCast_iff, cauchy_davenport_minOrder_add, Set.toENat_cardinalMk, R_apply, SimpleGraph.chromaticNumber_eq_biInf, SmoothPartitionOfUnity.sum_finsupport, Dynamics.coverMincard_le_netMaxcard, Order.coheight_coe_enat, ENat.mul_left_strictMono, Module.End.mem_genEigenspace_one, hasFTaylorSeriesUpToOn_succ_iff_left, Cardinal.enat_gc, Matroid.eRk_insert_eq_add_one, PowerSeries.le_order, contDiffOn_succ_iff_fderivWithin, SimpleGraph.eccent_le_iff, SimpleGraph.ediam_eq_top_of_not_preconnected, IsOpen.exists_contDiff_support_eq, Order.krullDim_eq_zero, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, Set.one_lt_encard_iff, ContinuousLinearEquiv.coe_toDiffeomorph, MvPowerSeries.order_mul_ge, Real.contDiff_rpow_const_of_le, exists_smooth_forall_mem_convex_of_local_const, ContDiffPointwiseHolderAt.contDiffAt, Cardinal.toENatAux_le_nat, ENat.map_coe, Cardinal.toENat_le_nat, Set.encard_pos, Order.krullDim_pos_iff_of_orderBot, SimpleGraph.ediam_def, SimpleGraph.egirth_le_length, ENat.toENNReal_max, Module.End.genEigenspace_div, CategoryTheory.injectiveDimension_eq_bot_iff, PartENat.withTopEquiv_zero, Set.encard_le_coe_iff, Continuous.exists_contDiff_approx, mdifferentiableAt_mulInvariantVectorField, contDiffOn_succ_iff_fderiv_apply, instIsContMDiffRiemannianBundleOfNatWithTopENat, ENat.isEmbedding_natCast, Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq, MvPowerSeries.ne_zero_iff_order_finite, SimpleGraph.chromaticNumber_top_eq_top_of_infinite, MvPowerSeries.le_weightedOrder, Module.End.genEigenspace_eq_genEigenspace_finrank_of_le, Set.encard_eq_two, SimpleGraph.chromaticNumber_le_sum_left, ENat.map_add, contMDiffWithinAt_infty, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, SmoothBumpCovering.support_toSmoothPartitionOfUnity_subset, ENat.floor_natCast_add, contDiff_succ_iff_deriv, MvPowerSeries.order_monomial, IsManifold.instOfNatWithTopENat_1, PartENat.withTopEquiv_symm_le, Module.End.HasUnifEigenvalue.of_mem_spectrum, ENat.toENNReal_pow, IsDiscreteValuationRing.addVal_eq_zero_of_unit, ENat.toENNReal_coe, ContMDiffMap.mdifferentiableAt, SimpleGraph.egirth_anti, contDiffOn_succ_iff_derivWithin, ENat.card_eq_one_iff_unique, ENat.toNat_eq_zero, Set.encard_lt_encard_iff_encard_diff_lt_encard_diff, SimpleGraph.IsClique.card_le_chromaticNumber, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, ENat.toNat_add, TestFunction.contDiff', Ideal.sup_height_eq_ringKrullDim, Dynamics.netMaxcard_univ, contDiffAt_zero, ENat.floor_sub_ofNat, Set.encard_pi_eq_prod_encard, ENat.floor_toENNReal_add, Nat.Prime.emultiplicity_one, SmoothBumpFunction.contMDiff, Set.encard_le_chainHeight_of_isChain, PartENat.toWithTop_ofNat, Dynamics.netMaxcard_eq_zero_iff, ENat.lift_coe, Module.End.Eigenvalues.val_mk, PowerSeries.coe_orderHom, Ideal.finiteHeight_iff_lt, Module.End.genEigenspace_nat, Order.height_int, Set.encard_diff, instContMDiffAddOfNatWithTopENat, eventuallyConst_iff_analyticOrderAt_sub_eq_top, SimpleGraph.vertexCoverNum_bot, SmoothPartitionOfUnity.finite_tsupport, instContMDiffMulOfNatWithTopENatOfContinuousMul, Matroid.eRk_singleton_eq, height_le_ringKrullDim_quotient_add_spanFinrank, IsManifold.instOfNatWithTopENat_2, Order.coheight_eq_coe_iff, Cardinal.toENat_comp_ofENat, ENat.floor_add_toENNReal, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, OpenPartialHomeomorph.contDiffOn_univBall_symm, ENat.card_fun, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, SimpleGraph.exists_walk_of_edist_ne_top, ENat.top_pow, ENat.strictMono_map_iff, contDiffWithinAt_abs, smoothSheaf.contMDiff_section, LeftInvariantDerivation.coe_zero, contDiff_infty_iff_deriv, SimpleGraph.radius_le_eccent, ENat.one_lt_top, Module.End.genEigenspace_le_maximal, ENat.floor_sub_one, ENat.toENNReal_iSup, Cardinal.toENat_le_iff_of_lt_aleph0, UpperHalfPlane.instIsManifoldComplexModelWithCornersSelfTopWithTopENat, ENat.toNat_coe, ENat.top_mul, Ideal.height_le_height_add_encard_of_subset, ENat.lt_floor, exists_embedding_euclidean_of_compact, analyticOrderAt_of_not_analyticAt, LeftInvariantDerivation.toDerivation_injective, Matroid.Dep.eRk_lt_encard, Module.End.mem_genEigenspace_nat, Metric.externalCoveringNumber_le_encard_self, LeftInvariantDerivation.evalAt_mul, Set.Finite.encard_biUnion, Nat.Prime.emultiplicity_mul, emultiplicity_eq_coe, emultiplicity_pow_prime_sub_pow_prime, Cardinal.ofENat_toENat_le, contDiff_of_differentiable_iteratedDeriv, Set.Finite.encard_eq_coe_toFinset_card, Module.length_eq_finrank, SimpleGraph.radius_eq_top_of_not_connected, analyticOrderAt_smul, Topology.RelCWComplex.iUnion_skeleton_eq_complex, analyticOrderAt_eq_zero, MvPowerSeries.order_add_of_order_ne, IsDiscreteValuationRing.addVal_def, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, Set.encard_insert_le, PartENat.ofENat_zero, Order.krullDim_eq_bot, SimpleGraph.radius_top, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing, Int.two_pow_two_pow_sub_pow_two_pow, Order.coheight_bot_eq_krullDim, Set.encard_le_one_iff, Order.height_le_iff, Cardinal.toENat_le_one, Set.encard_diff_singleton_add_one, emultiplicity_pow, PowerSeries.le_order_subst_right, PartENat.withTopEquiv_symm_coe, Metric.IsSeparated.encard_le_packingNumber, ENat.instCountable, Order.krullDim_eq_length_of_finiteDimensionalOrder, MvPowerSeries.order_prod, Set.encard_le_encard_of_injOn, Dynamics.coverMincard_finite_iff, AddMonoid.minOrder_eq_top, Set.encard_tsub_one_le_encard_diff_singleton, ENat.mul_le_mul_right_iff, Cardinal.zero_eq_ofENat, Cardinal.toENat_injOn, LinearIndepOn.encard_le_toENat_rank, Matroid.eRk_compl_union_add_eRk_compl_inter_le, ENat.ceil_add_one, Cardinal.toENat_eq_nat, contDiff_infty, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, Order.KrullDimLE.krullDim_le, Ring.ord_mul, Set.one_lt_encard_iff_nontrivial, emultiplicity_eq_iff_multiplicity_eq_of_ne_one, IsDiscreteValuationRing.addVal_one, MvPowerSeries.weightedOrder_zero, min_le_emultiplicity_add, ENat.add_biSup, SmoothPartitionOfUnity.mem_fintsupport_iff, Emetric.exists_smooth_forall_closedBall_subset, Ring.ord_one, minSmoothness_add, emultiplicity_pos_iff, Set.encard_diff_add_encard_inter, ringKrullDim_le_ringKrullDim_add_spanFinrank, UniformContinuous.exists_contDiff_dist_le, emultiplicity_eq_of_dvd_of_not_dvd, PowerSeries.order_eq_top, ENat.succ_def, PowerSeries.order_X, Cardinal.nat_le_ofENat, Cardinal.ofENat_toENat_eq_self, Topology.CWComplex.skeletonLT_zero_eq_empty, Order.IsMin.height_eq_zero, Metric.externalCoveringNumber_pos_iff, SimpleGraph.Reachable.coe_dist_eq_edist, ENat.mul_iInf', Order.coheight_anti, ENat.exists_nat_gt, IsLocalRing.maximalIdeal_height_eq_ringKrullDim, SimpleGraph.radius_bot, Cardinal.ofENat_toENat, ENat.toNat_eq_iff_eq_coe, contMDiffAt_infty, Function.Injective.encard_range, Order.krullDim_eq_one_iff_of_boundedOrder, Set.encard_le_one_iff_eq, Matroid.eRk_le_one_iff, Module.length_pi, Order.height_mono, Set.encard_add_encard_compl, Topology.RelCWComplex.skeletonLT_I, Cardinal.aleph_toENat, Order.height_le_iff', ENat.floor_eq_zero, Order.krullDim_nonneg, contMDiff_tangentBundleModelSpaceHomeomorph_symm, contDiffOn_succ_of_fderiv_apply, Matroid.eRk_singleton_eq_one_iff, Nat.Prime.emultiplicity_factorial_mul_succ, MvPowerSeries.order_eq_nat, Metric.coveringNumber_eq_zero, Order.coheight_pos, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, SimpleGraph.edist_eq_zero_iff, HasCompactSupport.exist_eLpNorm_sub_le_of_continuous, ENat.toNat_sub, ringKrullDim_eq_zero_of_field, Nat.emultiplicity_pow_sub_pow, LTSeries.height_last_longestOf, ENat.iInf_eq_zero, IsDiscreteValuationRing.addVal_le_iff_dvd, Ideal.height_le_height_add_spanFinrank_of_le, Real.deriv_arcsin_aux, PartENat.ofENat_top, Metric.packingNumber_pos_iff, contDiff_norm_rpow, exists_contDiff_tsupport_subset, Set.encard_le_encard, ENat.toENNReal_le, Cardinal.toENat_eq_iff_of_le_aleph0, Metric.externalCoveringNumber_le_coveringNumber, Order.index_le_height, MvPowerSeries.order_mul, Order.coheight_eq, ENat.forall_ne_top, SimpleGraph.le_egirth, ENat.instMeasurableSingletonClass, ContMDiffSection.mdifferentiableAt, Order.krullDim_le_one_iff_forall_isMin, minSmoothness_def, contDiffOn_infty_iff_deriv_of_isOpen, Nat.Prime.emultiplicity_pow_self, ENat.ceil_coe, SimpleGraph.diam_eq_zero, SimpleGraph.chromaticNumber_eq_iff_forall_surjective, Metric.encard_le_of_isSeparated, ENat.toNat_top, LeftInvariantDerivation.commutator_apply, PowerSeries.order_add_of_order_ne, Module.End.hasGenEigenvector_iff, Matroid.eRk_le_encard, ENat.floor_le_floor, Polynomial.ringKrullDim_of_isNoetherianRing, LeftInvariantDerivation.commutator_coe_derivation, Order.height_coe_withBot, ENat.tendsto_nhds_top_iff_natCast_lt, SimpleGraph.edist_le, SchwartzMap.smooth', Module.End.mem_genEigenspace_zero, MvPolynomial.ringKrullDim_of_isNoetherianRing, Set.encard_iUnion_le_of_fintype, Polynomial.trailingDegree_eq_natTrailingDegree, Monoid.le_minOrder, Set.one_le_encard_iff_nonempty, Submodule.FG.exists_span_set_encard_eq_spanFinrank, Ideal.height_le_spanRank_toENat, SimpleGraph.Reachable.exists_walk_length_eq_edist, Order.rev_index_le_coheight, ContMDiffSection.mdifferentiable, Mathlib.Tactic.ENatToNat.coe_add, Matroid.eq_loopyOn_iff_eRank, ENat.mul_top, MeasureTheory.Lp.dense_hasCompactSupport_contDiff, SmoothPartitionOfUnity.toPartitionOfUnity_toFun, ENat.add_left_injective_of_ne_top, Cardinal.natCast_eq_toENat_iff, SimpleGraph.radius_eq_top_of_isEmpty, cauchy_davenport_minOrder_mul, contDiff_infty_iff_fderiv, Topology.RelCWComplex.skeletonLT_top, ENat.eq_top_iff_forall_ge, Cardinal.ofENat_le_nat, ENat.coe_zero, Module.length_of_free_of_finite, ENat.sSup_eq_zero', ENat.map_zero, CategoryTheory.Retract.projectiveDimension_le, SimpleGraph.chromaticNumber_pathGraph, Metric.packingNumber_empty, Set.encard_insert_of_notMem, ENat.mul_le_mul_left_iff, LeftInvariantDerivation.ext_iff, Metric.coveringNumber_singleton, Module.End.genEigenspace_le_genEigenspace_finrank, Set.chainHeight_of_isEmpty, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, Module.End.mem_genEigenspace, ContDiffPointwiseHolderAt.zero_exponent_iff, le_emultiplicity_iff_replicate_subperm_primeFactorsList, Matroid.one_le_eRank, Set.encard_diff_singleton_of_mem, IsManifold.instLEInftyCastWithTopENat, Ideal.height_le_card_of_mem_minimalPrimes_span_finset, Cardinal.toENat_nat, MvPowerSeries.order_zero, MvPowerSeries.le_weightedOrder_subst_of_forall_ne_zero, Polynomial.trailingDegree_mul', Metric.coveringNumber_le_encard_self, Topology.RelCWComplex.skeletonLT_monotone, PowerSeries.order_mul, PowerSeries.nat_le_order, MvPowerSeries.weightedOrder_eq_top_iff, Set.chainHeight_eq_iSup, Ideal.height_le_ringKrullDim_of_ne_top, Diffeology.DSmooth.contDiff, ContDiffMapSupportedIn.iteratedFDerivLM_eq_of_scalars, Set.Finite.cast_ncard_eq, exists_smooth_zero_one_nhds_of_isClosed, emultiplicity_pow_self_of_prime, ENat.ceil_toENNReal_add, SimpleGraph.IsAcyclic.egirth_eq_top, SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum, contMDiffOn_vectorSpace_iff_contDiffOn, Module.End.genEigenspace_zero, Polynomial.le_trailingDegree_X_pow, Matroid.toENat_cRank_eq, Set.Finite.encard_biUnion_le, MvPowerSeries.le_order_pow, PowerSeries.order_X_pow, Ideal.height_bot, LeftInvariantDerivation.toFun_eq_coe, Order.height_eq_iSup_last_eq, Manifold.exists_lt_of_riemannianEDist_lt, ENat.toENNReal_iInf, Nat.emultiplicity_eq_card_pow_dvd, Order.height_enat, Set.chainHeight_eq_zero_iff, SimpleGraph.ediam_bot, SmoothBumpCovering.embeddingPiTangent_coe, Order.krullDim_of_noMinOrder, contDiffOn_infty_iff_derivWithin, SmoothPartitionOfUnity.nonneg', ENat.one_lt_card, ENat.self_le_mul_right, ENat.add_le_add_iff_left, Order.length_le_height_last, Cardinal.ofENat_zero, Order.coheight_eq_iSup_gt_coheight, AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero, ENat.mul_right_strictMono, contDiffOn_iff_continuousOn_differentiableOn_deriv, contMDiffOn_zero_iff, ringKrullDim_le_of_surjective, SimpleGraph.Walk.three_le_chromaticNumber_of_odd_loop, inTangentCoordinates_model_space, Metric.packingNumber_le_encard_self, ENat.zero_epow_top, SimpleGraph.edist_top_of_ne, Polynomial.trailingDegree_monomial, ENat.coe_add, minSmoothness_monotone, Order.krullDim_of_isSimpleOrder, Submodule.height_lt_top, Module.End.genEigenspace_le_smul, MvPowerSeries.min_order_le_add, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, SimpleGraph.edist_boxProd, Order.height_eq_top_iff, exists_contMDiffMap_one_nhds_of_subset_interior, PowerSeries.le_order_prod, MvPowerSeries.order_monomial_of_ne_zero, Mathlib.Tactic.ENatToNat.coe_one, Cardinal.ofENat_one, SmoothPartitionOfUnity.sum_le_one, contMDiffWithinAt_iff_nat, ContDiffPointwiseHolderAt.zero_order_iff, PowerSeries.order_add_of_order_eq, Polynomial.trailingDegree_eq_top, Module.supportDim_le_of_surjective, Cardinal.ofNat_eq_ofENat, Order.length_le_coheight_head, Matrix.eRank_submatrix_le, Module.End.genEigenspace_restrict, SimpleGraph.chromaticNumber_mono_of_hom, ENat.ceil_le_floor_add_one, Topology.RelCWComplex.closedCell_subset_skeleton, SchwartzMap.smooth, Real.contDiffAt_arccos_iff, Matroid.eRk_submod, PartENat.withTopEquiv_symm_lt, Monoid.minOrder_le_orderOf, SimpleGraph.chromaticNumber_eq_one_iff, Order.krullDim_eq_zero_iff_of_orderBot, TestFunctionClass.map_contDiff, Dynamics.one_le_netMaxcard_iff, PartENat.withTopEquiv_symm_top, Metric.coveringNumber_anti, Cardinal.natCast_le_toENat_iff, Polynomial.trailingDegree_one_le, ENat.ceil_eq_zero, ENat.add_biSup', exists_contMDiffMap_forall_mem_convex_of_local_const, Stream'.Seq.lt_length'_iff, smooth_functions_tower, Set.Finite.encard_strictMonoOn, padicValNat.maxPowDiv_eq_emultiplicity, Module.supportDim_eq_bot_of_subsingleton, ENat.add_lt_add_iff_right, multiplicity_le_emultiplicity, instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, SimpleGraph.edist_eq_one_iff_adj, Set.encard_le_one_iff_subsingleton, Mathlib.Meta.Positivity.natCeil_pos, ENat.biSup_add, MvPowerSeries.weightedOrder_prod, Set.encard_singleton, Order.bot_lt_krullDim_iff, AddMonoid.minOrder_le_natCard, inCoordinates_tangent_bundle_core_model_space, PowerSeries.le_weightedOrder_subst, MvPowerSeries.weightedOrder_one, Order.height_eq_coe_iff_minimal_le_height, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, ENat.lt_coe_add_one_iff, ContDiffMapSupportedIn.structureMapLM_apply, ENat.card_le_one, Polynomial.le_trailingDegree_X, Module.length_eq_rank, ContDiffBump.contDiffWithinAt, Dynamics.le_coverMincard_image, LeftInvariantDerivation.instLinearMapClassContMDiffMapModelWithCornersSelfSomeENatTop, LeftInvariantDerivation.coeFnAddMonoidHom_apply, Monoid.minOrder_eq_top, contMDiff_snd_tangentBundle_modelSpace, Monoid.minOrder_eq_top_iff, emultiplicity_mul, SimpleGraph.eccent_def, Matroid.spanning_iff_eRk_le, SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective, Cardinal.toENat_lt_top, IsManifold.instOfNatWithTopENat, contDiff_sigmoid, MvPowerSeries.le_order_pow_of_constantCoeff_eq_zero, Polynomial.trailingDegree_X_pow, MonoidWithZeroHom.ENatMap_apply, instLieGroupOfNatWithTopENat, Derivation.evalAt_apply, Order.one_lt_height_iff, Polynomial.IsDistinguishedAt.coe_natDegree_eq_order_map, Order.coheight_le_iff, natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero, ENat.iSup_coe_lt_top, Polynomial.trailingDegree_X, Cardinal.toENat_congr, Polynomial.emultiplicity_le_one_of_separable, ENat.range_natCast, SimpleGraph.eccent_eq_zero_of_subsingleton, analyticOrderAt_add_of_ne, contMDiffOn_infty, ENat.isOpenEmbedding_natCast, PowerSeries.order_monomial_of_ne_zero, PowerSeries.le_order_subst_left, ContDiffMapSupportedIn.structureMapLM_eq, ENat.one_le_iff_ne_zero, contDiff_succ_iff_hasFDerivAt, Order.krullDim_nat, padicValNat_eq_emultiplicity, ENat.lt_one_iff_eq_zero, Matroid.toENat_cRk_eq, ENat.floor_le, Set.encard_le_encard_diff_add_encard, ringKrullDim_le_ringKrullDim_quotient_add_encard, SmoothBumpCovering.toSmoothPartitionOfUnity_zero_of_zero, contDiffAt_abs, contDiff_one_iff_deriv, SimpleGraph.edist_bot_of_ne, SmoothPartitionOfUnity.contMDiff_sum, Order.krullDimLE_iff, ENat.card_eq_coe_natCard, Cardinal.toENat_eq_one, Metric.exists_contMDiffMap_forall_closedEBall_subset, ENat.exists_ne_top, ENat.epow_zero, ENat.not_lt_zero, contDiffWithinAt_succ_iff_hasFDerivWithinAt, ENat.one_epow, SimpleGraph.eccent_top, Polynomial.trailingDegree_mul, ENat.top_mul', Order.krullDim_eq_top_iff, Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq_of_pos, SimpleGraph.chromaticNumber_bot, SimpleGraph.edist_le_one_iff_adj_or_eq, Real.smoothTransition.contDiff, ENat.coe_lt_top, Cardinal.nat_lt_ofENat, SimpleGraph.radius_eq_iInf_iSup_edist, PowerSeries.order_eq_nat, WithBot.add_one_le_iff, Metric.coveringNumber_le_one_of_ediam_le, Set.chainHeight_eq_top_iff, Diffeology.dSmooth_iff_contDiff, LinearMap.IsSymmetric.eigenvectorBasis_def, LeftInvariantDerivation.evalAt_apply, AnalyticAt.analyticOrderAt_eq_zero, MvPowerSeries.le_order_map, Dynamics.coverMincard_monotone_subset
|