| Metric | Count |
|---|
DefinitionsENatMap, ENatMap, instSuccAddOrder, instUniqueUnits, instWellFoundedRelation, map, toNat, toNatHom, ENatMap, ENatMap, ENatMap, ENatMap, instBotENat, instCanonicallyOrderedAddENat, instCharZeroENat, instCommSemiringENat, instIsOrderedRingENat, instLinearOrderENat, instLinearOrderedAddCommMonoidWithTopENat, instNoZeroDivisorsENat, instNontrivialENat, instOrderBotENat, instOrderTopENat, instOrderedSubENat, instSubENat, instSuccOrderENat, instWellFoundedLTENat, instZeroENat | 28 |
TheoremsENatMap_apply, ENatMap_apply, addLECancellable_coe, addLECancellable_of_lt_top, addLECancellable_of_ne_top, add_le_add_iff_left, add_le_add_iff_right, add_left_injective_of_ne_top, add_lt_add_iff_left, add_lt_add_iff_right, add_lt_top, add_one_eq_coe_top_iff, add_one_le_iff, add_one_natCast_le_withTop_of_lt, add_one_pos, add_right_injective_of_ne_top, canLift, coe_add, coe_inj, coe_le_coe, coe_lift, coe_lt_coe, coe_lt_top, coe_mul, coe_ne_top, coe_one, coe_sub, coe_toNat, coe_toNatHom, coe_toNat_eq_self, coe_toNat_le_self, coe_top_add_one, coe_zero, eq_of_forall_natCast_le_iff, eq_top_iff_forall_ge, eq_top_iff_forall_gt, eq_top_iff_forall_ne, eq_top_of_pow, exists_nat_gt, exists_ne_top, forall_natCast_le_iff_le, forall_ne_top, le_coe_iff, le_lift_iff, le_sub_of_add_le_left, le_sub_of_add_le_right, le_sub_one_of_lt, lift_add, lift_coe, lift_eq_toNat_of_lt_top, lift_le_iff, lift_lt_iff, lift_ofNat, lift_one, lift_zero, lt_add_one_iff, lt_add_one_iff', lt_coe_add_one_iff, lt_lift_iff, lt_one_iff_eq_zero, map_add, map_coe, map_eq_top_iff, map_natCast_eq_zero, map_natCast_inj, map_natCast_injective, map_natCast_mul, map_natCast_nonneg, map_natCast_strictMono, map_ofNat, map_one, map_top, map_zero, monotone_map_iff, mul_le_mul_left_iff, mul_le_mul_of_le_right, mul_le_mul_right_iff, mul_left_strictMono, mul_right_strictMono, mul_top, mul_top', natCast_le_of_coe_top_le_withTop, natCast_lt_of_coe_top_le_withTop, natCast_lt_succ, natCast_ne_coe_top, nat_induction, ne_top_iff_exists, not_lt_zero, ofNat_ne_top, one_le_iff_ne_zero, one_le_iff_ne_zero_withTop, one_lt_top, one_ne_top, pow_eq_top_iff, pow_lt_top_iff, pow_ne_top_iff, recTopCoe_ofNat, recTopCoe_one, recTopCoe_zero, self_le_mul_left, self_le_mul_right, some_eq_coe, strictMono_map_iff, sub_eq_top_iff, sub_ne_top_iff, sub_sub_cancel, sub_top, succ_def, toNatHom_apply, toNat_add, toNat_coe, toNat_eq_iff, toNat_eq_iff_eq_coe, toNat_eq_zero, toNat_le_of_le_coe, toNat_le_toNat, toNat_mul, toNat_ofNat, toNat_one, toNat_sub, toNat_top, toNat_zero, top_mul, top_mul', top_ne_coe, top_ne_ofNat, top_ne_one, top_ne_zero, top_pos, top_pow, top_sub_coe, top_sub_ofNat, top_sub_one, zero_ne_top, ENatMap_apply, ENatMap_apply, add_one_le_iff, lt_add_one_iff | 138 |
| Total | 166 |
| Name | Category | Theorems |
|---|
instBotENat 📖 | CompOp | — |
instCanonicallyOrderedAddENat 📖 | CompOp | 5 mathmath: Order.krullDim_le_of_krullDim_preimage_le, tangentBundleCore.isContMDiff, TangentBundle.contMDiffVectorBundle, Polynomial.ringKrullDim_le, Order.krullDim_le_of_krullDim_preimage_le'
|
instCharZeroENat 📖 | CompOp | — |
instCommSemiringENat 📖 | CompOp | 559 mathmath: TangentBundle.continuousLinearMapAt_model_space, Order.coheight_add_one_le, ENat.add_lt_top, Cardinal.natCast_lt_toENat_iff, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ, instLieAddGroupOfNatWithTopENat, Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity, Order.LTSeries.length_le_krullDim, SimpleGraph.vertexCoverNum_le_card_sub_one, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, ENat.lt_add_one_iff', ringKrullDim_succ_le_ringKrullDim_polynomial, Set.toENat_cardinalMk_subtype, ENat.self_le_mul_left, instIsContMDiffRiemannianBundleOfNatWithTopENat_1, Cardinal.toENat_eq_natCast_iff, Order.krullDim_lt_coe_iff, ENat.toNat_one, Set.encard_diff_add_encard, ENat.coe_one, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ENat.card_prod, Set.encard_union_eq, ENat.iInf_mul_of_ne, Set.encard_prod, CategoryTheory.injectiveDimension_le_iff, MvPowerSeries.le_order_mul, LinearMap.IsSymmetric.diagonalization_apply_self_apply, PartENat.ofENat_one, Cardinal.toENat_ofENat, Matroid.eRk_singleton_le, ENat.ceil_add_ofNat, Ring.krullDimLE_iff, ringKrullDim_eq_one_iff_of_isLocalRing_isDomain, contMDiff_addInvariantVectorField, Cardinal.one_eq_ofENat, Module.length_of_free, PowerSeries.order_expand, ENat.iSup_add_iSup_of_monotone, ENat.natCast_le_of_coe_top_le_withTop, Order.height_add_one_le, ENat.one_lt_card_iff_nontrivial, ENat.map_one, Matroid.eRank_le_encard_add_eRk_compl, ENat.floor_add_ofNat, PartENat.withTopEquiv_one, contMDiff_mulInvariantVectorField, ENat.coe_top_add_one, Order.krullDim_le_one_iff, Module.supportDim_add_length_eq_supportDim_of_isRegular, Dynamics.coverMincard_univ, contDiff_one_iff_fderiv, contMDiff_equivTangentBundleProd_symm, Submodule.spanRank_toENat_eq_iInf_encard, Real.contDiffAt_rpow_const_of_le, ENat.ceil_add_natCast, Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown, LinearMap.IsSymmetric.directSum_decompose_apply, MvPowerSeries.le_weightedOrder_mul, contMDiff_infty, Cardinal.toENat_eq_zero, contDiffOn_nat_iff_continuousOn_differentiableOn_deriv, MvPowerSeries.le_order_prod, ENat.floor_add_one, Order.le_krullDim_iff, Cardinal.toENat_eq_ofNat, PowerSeries.order_mul_ge, Set.encard_union_add_encard_inter, ENat.floor_add_natCast, WithBot.lt_add_one_iff, contDiffWithinAt_nat, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, Matroid.IsNonloop.eRk_eq, ENat.mul_iSup, ringKrullDim_succ_le_ringKrullDim_powerseries, contDiffOn_infty, Polynomial.height_eq_height_add_one, MvPowerSeries.le_weightedOrder_prod, Dynamics.one_le_coverMincard_iff, tangentBundle_model_space_coe_chartAt, ENat.ceil_sub_one, contDiff_iff_forall_nat_le, Nat.Prime.emultiplicity_le_emultiplicity_choose_add, ENat.epow_natCast, contDiff_succ_iff_fderiv, contMDiffAt_mulInvariantVectorField, IsContDiffImplicitAt.one_le, ENat.biSup_add', FiniteMultiplicity.emultiplicity_self, MvPowerSeries.weightedOrder_mul, ENat.sum_iSup, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, Topology.RelCWComplex.iUnion_openCell_eq_skeleton, Dynamics.netMaxcard_zero, ENat.iInf_mul', Nat.two_pow_sub_pow, ENat.add_right_injective_of_ne_top, mdifferentiableAt_addInvariantVectorField, Matroid.eRk_dual_add_eRank', Nat.Prime.emultiplicity_factorial_mul, ENat.one_le_card_iff_nonempty, AddHom.ENatMap_apply, contDiffAt_one_iff, Order.coheight_eq_coe_add_one_iff, Mathlib.Tactic.ENatToNat.coe_mul, ENat.card_le_one_iff_subsingleton, Cardinal.toENat_lt_natCast_iff, Metric.externalCoveringNumber_le_one_of_ediam_le, SimpleGraph.eccent_le_one_iff, ENat.lift_one, Matroid.eRk_le_eRk_add_eRk_diff, contDiff_all_iff_nat, Set.encard_union_le, contDiffOn_succ_of_fderivWithin, IsPrincipalIdealRing.height_eq_one_of_isMaximal, emultiplicity_pow_prime_pow_sub_pow_prime_pow, ENat.epow_mul, Cardinal.toENat_lift, Matroid.eRk_compl_insert_union_add_eRk_compl_insert_inter_le, ENat.add_one_le_iff, Int.emultiplicity_pow_sub_pow, Stream'.Seq.length'_cons, SimpleGraph.edist_top, MvPowerSeries.one_le_order_iff_constCoeff_eq_zero, SimpleGraph.vertexCoverNum_top, mdifferentiable_mulInvariantVectorField, Nat.emultiplicity_pow_add_pow, ENat.iInf_mul, Cardinal.toENat_le_ofNat, Matroid.eRk_insert_le_add_one, Ideal.height_le_height_add_of_liesOver, ENat.epow_add, MvPowerSeries.le_order_subst, MvPowerSeries.le_weightedOrder_pow, ENat.add_iSup, Module.End.hasUnifEigenvalue_iff_mem_spectrum, CategoryTheory.injectiveDimension_ge_iff, contDiffOn_nat_iff_continuousOn_differentiableOn, Ideal.height_le_height_add_one_of_mem, ENat.mul_sSup, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, Matroid.exists_eRk_insert_eq_add_one_of_lt, Module.End.Eigenvalues.mk_val, LinearMap.IsSymmetric.diagonalization_symm_apply, Matroid.eRk_inter_add_eRk_union_le, Module.End.genEigenspace_inf_le_add, contMDiff_vectorSpace_iff_contDiff, ringKrullDim_succ_le_of_surjective, ENat.top_sub_one, ENat.instContinuousMul, TangentBundle.coordChange_model_space, Matroid.eRk_dual_add_eRank, Cardinal.one_le_ofENat, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, instContMDiffInv₀OfNatWithTopENat, CategoryTheory.projectiveDimension_lt_iff, Metric.coveringNumber_eq_one_of_ediam_le, RingHom.ENatMap_apply, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, Set.encard_diff_add_encard_of_subset, SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable, Topology.RelCWComplex.openCell_subset_skeletonLT, Topology.RelCWComplex.closedCell_subset_skeletonLT, PowerSeries.le_order_mul, ENat.instContinuousAdd, contDiffOn_succ_iff_fderiv_of_isOpen, ENat.mul_le_mul_of_le_right, ENat.map_natCast_mul, hasFTaylorSeriesUpToOn_succ_iff_right, ENat.add_sSup, PartENat.toWithTop_add, IsDiscreteValuationRing.addVal_uniformizer, contDiff_nat_iff_iteratedDeriv, Cardinal.ofENat_add, ENat.coe_mul, instIsManifoldMinSmoothnessOfNatWithTopENat_1, ENat.ceil_add_le, AnalyticAt.analyticOrderAt_deriv_add_one, Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors, Order.krullDim_WithTop, contDiffPointwiseHolderAt_iff, Matroid.eRk_insert_inter_add_eRk_insert_union_le, ringKrullDim_le_ringKrullDim_quotient_add_card, Dynamics.coverMincard_zero, ENat.natCast_lt_succ, PowerSeries.one_le_order_iff_constCoeff_eq_zero, Ideal.height_le_ringKrullDim_quotient_add_one, ENat.toENNRealRingHom_apply, instContMDiffVectorBundleOfNatWithTopENat, trivializationAt_model_space_apply, hasFTaylorSeriesUpToOn_top_iff, analyticOrderAt_mul, SimpleGraph.ediam_top, ENat.coe_toNatHom, Polynomial.le_trailingDegree_mul, ENat.ceil_natCast_add, hasFTaylorSeriesUpTo_succ_nat_iff_right, Order.coheight_coe_withTop, Dynamics.coverMincard_union_le, Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ, ENat.mul_top', hasFTaylorSeriesUpToOn_succ_nat_iff_right, Cardinal.ofENat_eq_one, 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, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, Cardinal.ofENat_mul, PartENat.toWithTop_one, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, instIsContMDiffRiemannianBundleOfNatWithTopENat_2, Order.height_eq_coe_iff, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', SimpleGraph.ediam_eq_one, AddMonoidHom.ENatMap_apply, ENat.floor_one, SimpleGraph.edist_triangle, Matrix.eRank_subsingleton, tangentBundle_model_space_coe_chartAt_symm, tangentBundleModelSpaceHomeomorph_coe, MvPowerSeries.weightedOrder_mul_ge, ENat.card_sum, Set.one_le_encard_insert, IsManifold.instLEInftyOfNatWithTopENat_1, ENat.toNatHom_apply, ENat.mul_iInf_of_ne, Nat.Prime.emultiplicity_self, IsDiscreteValuationRing.addVal_mul, ENat.mul_epow, tangentBundleCore_coordChange_model_space, Module.length_eq_one, Metric.externalCoveringNumber_eq_one_of_ediam_le, ENat.epow_one, ENat.ceil_add_toENNReal, Module.End.genEigenspace_one, contDiffOn_all_iff_nat, instIsManifoldMinSmoothnessOfNatWithTopENat, ringKrullDim_add_length_eq_ringKrullDim_of_isRegular, 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', Matroid.eRk_union_le_eRk_add_eRk, Matroid.eRk_le_eRk_inter_add_eRk_diff, instContMDiffMulOfNatWithTopENat, Cardinal.toNat_toENat, Manifold.riemannianEDist_def, Ideal.height_le_ringKrullDim_quotient_add_encard, Ideal.primeHeight_add_one_le_of_lt, Set.one_le_chainHeight_iff, tangentBundleCore.isContMDiff, 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, emultiplicity_geom_sum₂_eq_one, TangentBundle.contMDiffVectorBundle, Module.supportDim_quotSMulTop_succ_eq_supportDim, Matroid.IsCircuit.eRk_add_one_eq, SimpleGraph.ediam_le_two_mul_radius, PartENat.withTopEquiv_symm_one, contDiffAt_succ_iff_hasFDerivAt, toENat_rank_span_set, ENat.epow_eq_one_iff, ENat.iSup_mul, ENat.add_lt_add_iff_left, Set.encard_singleton_inter, Dynamics.coverMincard_le_pow, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, Dynamics.coverMincard_mul_le_pow, contDiffWithinAt_infty, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson, tangentBundle_model_space_chartAt, Module.length_eq_one_iff, ENat.one_le_epow, contMDiffAt_iff_nat, Cardinal.toENat_strictMonoOn, LinearMap.IsSymmetric.direct_sum_isInternal, Matroid.eRk_eq_one_iff, ENat.toNat_mul, Metric.externalCoveringNumber_singleton, IsPrincipalIdealRing.ringKrullDim_eq_one, Real.contDiffAt_rpow_const, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, ENat.sSup_add, IsDiscreteValuationRing.addVal_pow, ENat.addLECancellable_coe, Submodule.spanRank_toENat_eq_iInf_finset_card, ENat.pow_lt_top_iff, Module.length_finsupp, PowerSeries.le_order_pow, analyticOrderAt_pow, Order.one_le_krullDim_iff, squarefree_iff_emultiplicity_le_one, Set.encard_eq_one, ENat.toENNReal_one, Cardinal.continuum_toENat, ringKrullDim_le_ringKrullDim_add_card, analyticOrderAt_id, Set.encard_eq_add_one_iff, PowerSeries.order_pow, CategoryTheory.projectiveDimension_le_iff, SimpleGraph.chromaticNumber_le_one_of_subsingleton, ENat.toENNReal_add, contMDiffAt_vectorSpace_iff_contDiffAt, MvPowerSeries.order_expand, ENat.recTopCoe_one, ENat.iSup_add, Set.encard_ne_add_one, Module.supportDim_le_supportDim_quotSMulTop_succ, CategoryTheory.projectiveDimension_ge_iff, mdifferentiable_addInvariantVectorField, ENat.lt_add_one_iff, ENat.addLECancellable_of_ne_top, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, Module.length_prod, AnalyticAt.analyticOrderAt_comp, Matroid.eRank_add_eRank_dual, Int.emultiplicity_pow_add_pow, contDiffAt_infty, TangentBundle.symmL_model_space, PowerSeries.le_order_subst, ENat.pow_eq_top_iff, CategoryTheory.injectiveDimension_lt_iff, Polynomial.ringKrullDim_le, ENat.mul_iInf, Cardinal.toENat_le_iff_of_le_aleph0, ENat.sSup_mul, contDiff_nat_iff_continuous_differentiable, Cardinal.toENat_eq_top, ENat.le_sub_one_of_lt, differentiableWithinAt_localInvariantProp, contDiffWithinAt_iff_forall_nat_le, ENat.add_one_pos, SimpleGraph.eq_top_iff_forall_eccent_eq_one, Cardinal.one_lt_ofENat, Topology.CWComplex.iUnion_openCell_eq_skeleton, ENat.ceil_one, Ideal.map_height_le_one_of_mem_minimalPrimes, tangentBundleModelSpaceHomeomorph_coe_symm, PartENat.toWithTop_one', contDiff_one_iff_hasFDerivAt, Int.two_pow_sub_pow, MeasureTheory.stoppedProcess_eq', Order.krullDim_le_one_iff_forall_isMax, Order.krullDim_withBot, Matroid.eRk_union_le_encard_add_eRk, Cardinal.ofENat_le_one, Metric.packingNumber_singleton, contMDiff_equivTangentBundleProd, instIsManifoldOfNatWithTopENatOfMinSmoothness_1, SubAddAction.ENat_card_ofStabilizer_add_zero_eq, Nat.Prime.emultiplicity_pow, Matroid.eRk_union_le_eRk_add_encard, ringKrullDim_nat, Module.length_eq_add_of_exact, ENat.add_le_add_iff_right, ENat.toENNReal_mul, Cardinal.toENat_le_natCast_iff, Set.toENat_cardinalMk, ENat.mul_left_strictMono, Module.End.mem_genEigenspace_one, hasFTaylorSeriesUpToOn_succ_iff_left, Cardinal.enat_gc, Matroid.eRk_insert_eq_add_one, contDiffOn_succ_iff_fderivWithin, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, Set.one_lt_encard_iff, MvPowerSeries.order_mul_ge, Real.contDiff_rpow_const_of_le, ContDiffPointwiseHolderAt.contDiffAt, Cardinal.toENat_le_nat, hasFTaylorSeriesUpTo_top_iff, Module.End.genEigenspace_div, mdifferentiableAt_mulInvariantVectorField, contDiffOn_succ_iff_fderiv_apply, ENat.map_add, contMDiffWithinAt_infty, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, ENat.floor_natCast_add, contDiff_succ_iff_deriv, IsManifold.instOfNatWithTopENat_1, Module.End.HasUnifEigenvalue.of_mem_spectrum, ENat.toENNReal_pow, contDiffOn_succ_iff_derivWithin, ENat.card_eq_one_iff_unique, ENat.toNat_add, Dynamics.netMaxcard_univ, Set.encard_pi_eq_prod_encard, ENat.floor_toENNReal_add, Module.End.Eigenvalues.val_mk, PowerSeries.coe_orderHom, instContMDiffAddOfNatWithTopENat, 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, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, ENat.top_pow, ENat.one_lt_top, ENat.addLECancellable_of_lt_top, ENat.floor_sub_one, Cardinal.toENat_le_iff_of_lt_aleph0, ENat.top_mul, Ideal.height_le_height_add_encard_of_subset, Nat.Prime.emultiplicity_mul, emultiplicity_pow_prime_sub_pow_prime, Cardinal.ofENat_toENat_le, analyticOrderAt_smul, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, Set.encard_insert_le, SimpleGraph.radius_top, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing, Int.two_pow_two_pow_sub_pow_two_pow, Set.encard_le_one_iff, Cardinal.toENat_le_one, Set.encard_diff_singleton_add_one, emultiplicity_pow, Order.krullDim_eq_length_of_finiteDimensionalOrder, Set.encard_tsub_one_le_encard_diff_singleton, ENat.mul_le_mul_right_iff, 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, ENat.add_biSup, minSmoothness_add, Set.encard_diff_add_encard_inter, ringKrullDim_le_ringKrullDim_add_spanFinrank, ENat.succ_def, PowerSeries.order_X, Cardinal.ofENat_toENat_eq_self, ENat.mul_iInf', Cardinal.ofENat_toENat, ENat.sum_iSup_of_monotone, contMDiffAt_infty, Order.krullDim_eq_one_iff_of_boundedOrder, Set.encard_le_one_iff_eq, Matroid.eRk_le_one_iff, Module.length_pi, Set.encard_add_encard_compl, Cardinal.aleph_toENat, contMDiff_tangentBundleModelSpaceHomeomorph_symm, contDiffOn_succ_of_fderiv_apply, Matroid.eRk_singleton_eq_one_iff, Nat.Prime.emultiplicity_factorial_mul_succ, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, Nat.emultiplicity_pow_sub_pow, Ideal.height_le_height_add_spanFinrank_of_le, contDiff_norm_rpow, Cardinal.toENat_eq_iff_of_le_aleph0, MvPowerSeries.order_mul, Order.krullDim_le_one_iff_forall_isMin, Polynomial.ringKrullDim_of_isNoetherianRing, Order.height_coe_withBot, MvPolynomial.ringKrullDim_of_isNoetherianRing, Set.one_le_encard_iff_nonempty, Ideal.height_le_spanRank_toENat, Mathlib.Tactic.ENatToNat.coe_add, ENat.mul_top, ENat.add_left_injective_of_ne_top, Cardinal.natCast_eq_toENat_iff, Module.length_of_free_of_finite, Set.encard_insert_of_notMem, ENat.mul_le_mul_left_iff, Metric.coveringNumber_singleton, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, ContDiffPointwiseHolderAt.zero_exponent_iff, Matroid.one_le_eRank, Set.encard_diff_singleton_of_mem, IsManifold.instLEInftyCastWithTopENat, Cardinal.toENat_nat, Polynomial.trailingDegree_mul', PowerSeries.order_mul, ENat.ceil_toENNReal_add, contMDiffOn_vectorSpace_iff_contDiffOn, Matroid.toENat_cRank_eq, MvPowerSeries.le_order_pow, Manifold.exists_lt_of_riemannianEDist_lt, ENat.one_lt_card, ENat.self_le_mul_right, ENat.add_le_add_iff_left, Order.coheight_eq_iSup_gt_coheight, AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero, ENat.mul_right_strictMono, inTangentCoordinates_model_space, SimpleGraph.edist_top_of_ne, ENat.coe_add, Order.krullDim_of_isSimpleOrder, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, SimpleGraph.edist_boxProd, Mathlib.Tactic.ENatToNat.coe_one, Cardinal.ofENat_one, contMDiffWithinAt_iff_nat, ENat.ceil_le_floor_add_one, Matroid.eRk_submod, ENat.natCast_lt_of_coe_top_le_withTop, SimpleGraph.chromaticNumber_eq_one_iff, Dynamics.one_le_netMaxcard_iff, Cardinal.natCast_le_toENat_iff, hasFTaylorSeriesUpToOn_top_iff_add, ENat.add_biSup', ENat.add_lt_add_iff_right, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, SimpleGraph.edist_eq_one_iff_adj, Set.encard_le_one_iff_subsingleton, ENat.biSup_add, Set.encard_singleton, inCoordinates_tangent_bundle_core_model_space, PowerSeries.le_weightedOrder_subst, ENat.lt_coe_add_one_iff, ENat.card_le_one, Polynomial.le_trailingDegree_X, Module.length_eq_rank, contMDiff_snd_tangentBundle_modelSpace, emultiplicity_mul, Cardinal.toENat_lt_top, MonoidWithZeroHom.ENatMap_apply, instLieGroupOfNatWithTopENat, Order.one_lt_height_iff, Polynomial.trailingDegree_X, Cardinal.toENat_congr, Polynomial.emultiplicity_le_one_of_separable, contMDiffOn_infty, ENat.one_le_iff_ne_zero, contDiff_succ_iff_hasFDerivAt, Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one, ENat.lt_one_iff_eq_zero, Matroid.toENat_cRk_eq, Set.encard_le_encard_diff_add_encard, ringKrullDim_le_ringKrullDim_quotient_add_encard, contDiff_one_iff_deriv, Order.krullDimLE_iff, Cardinal.toENat_eq_one, ENat.epow_zero, contDiffWithinAt_succ_iff_hasFDerivWithinAt, ENat.one_epow, SimpleGraph.eccent_top, Polynomial.trailingDegree_mul, ENat.top_mul', SimpleGraph.chromaticNumber_bot, SimpleGraph.edist_le_one_iff_adj_or_eq, WithBot.add_one_le_iff, Metric.coveringNumber_le_one_of_ediam_le, LinearMap.IsSymmetric.eigenvectorBasis_def
|
instIsOrderedRingENat 📖 | CompOp | — |
instLinearOrderENat 📖 | CompOp | 310 mathmath: Function.Embedding.encard_le, ENat.add_lt_top, Cardinal.natCast_lt_toENat_iff, ENat.toENNReal_lt_top, emultiplicity_le_emultiplicity_of_dvd_left, ENat.top_pos, ENat.lt_add_one_iff', Set.toENat_cardinalMk_subtype, ENat.self_le_mul_left, Cardinal.toENat_eq_natCast_iff, ENat.card_le_card_of_injective, Cardinal.ofENat_lt_ofNat, Set.tsub_encard_le_encard_diff, Matrix.eRank_le_card_width, AddCircle.card_torsion_le_of_isSMulRegular, ENat.card_lt_top, MvPowerSeries.le_order_mul, Cardinal.ofENat_le_ofNat, Cardinal.toENat_ofENat, Set.ncard_le_encard, Module.length_of_free, Matrix.eRank_le_card_height, emultiplicity_add_eq_min, Module.End.independent_genEigenspace, ENat.card_pos, ENat.toENNReal_strictMono, Finset.set_encard_biUnion_le, ENat.one_lt_card_iff_nontrivial, Set.encard_preimage_val_le_encard_left, Module.End.genEigenspace_directed, lt_emultiplicity_of_lt_multiplicity, ENat.monotone_map_iff, Submodule.spanRank_toENat_eq_iInf_encard, Topology.RelCWComplex.coe_skeletonLT, Module.End.maxGenEigenspace_eq, Nat.count_le_setENCard, MvPowerSeries.le_weightedOrder_mul, Cardinal.toENat_eq_zero, MvPowerSeries.le_order_prod, Topology.CWComplex.iUnion_openCell_eq_skeletonLT, emultiplicity_lt_iff_not_dvd, Cardinal.toENat_eq_ofNat, emultiplicity_le_emultiplicity_of_dvd_right, Module.End.maxGenEigenspace_eq_genEigenspace_finrank, emultiplicity_pos_of_dvd, Module.End.mapsTo_genEigenspace_of_comm, PowerSeries.order_mul_ge, ENat.forall_natCast_le_iff_le, WithBot.lt_add_one_iff, Cardinal.ofENat_mono, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, Set.encard_preimage_val_le_encard_right, PowerSeries.le_order_smul, PowerSeries.order_finite_iff_ne_zero, Polynomial.le_trailingDegree_C, MvPowerSeries.le_weightedOrder_prod, Nat.Prime.emultiplicity_le_emultiplicity_choose_add, ENat.map_natCast_strictMono, Topology.RelCWComplex.iUnion_openCell_eq_skeleton, MvPowerSeries.le_weightedOrder_map, le_emultiplicity_map, Stream'.Seq.length'_le_iff, Cardinal.ofENat_lt_aleph0, MvPowerSeries.nat_le_order, ENat.one_le_card_iff_nonempty, Mathlib.Tactic.ENatToNat.not_lt_top, ENat.card_le_one_iff_subsingleton, Cardinal.toENat_lt_natCast_iff, Polynomial.le_trailingDegree_monomial, Set.Finite.encard_lt_top, ENat.card_lt_top_of_finite, Submodule.inf_genEigenspace, MvPowerSeries.nat_le_weightedOrder, Set.encard_union_le, Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex, Set.encard_strictMono, Polynomial.trailingDegree_le_trailingDegree, Order.krullDim_le_of_krullDim_preimage_le, Cardinal.toENat_lift, ENat.add_one_le_iff, ENat.instOrderTopology, MvPowerSeries.one_le_order_iff_constCoeff_eq_zero, Cardinal.toENat_le_ofNat, MvPowerSeries.le_weightedOrder_pow, le_emultiplicity_of_le_multiplicity, PowerSeries.le_order_map, emultiplicity_le_emultiplicity_iff, MvPowerSeries.min_weightedOrder_le_add, Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt, ENat.eq_top_iff_forall_gt, LinearMap.finrank_genEigenspace_le, Module.End.iSup_genEigenspace_eq, Module.End.genEigenspace_inf_le_add, ENat.coe_toNat_le_self, Module.End.eigenspace_le_genEigenspace, Cardinal.one_le_ofENat, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, ENat.epow_right_mono, PowerSeries.le_order_mul, Set.encard_lt_top_iff, Set.encard_le_card, Set.Finite.encard_lt_encard, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, ENat.natCast_lt_succ, PowerSeries.one_le_order_iff_constCoeff_eq_zero, ENat.toENNRealOrderEmbedding_apply, Nat.emultiplicity_two_factorial_lt, le_emultiplicity_of_pow_dvd, MvPowerSeries.le_weightedOrder_smul, Polynomial.le_trailingDegree_mul, ENat.mul_top', Stream'.Seq.at_least_as_long_as_coind, Module.End.disjoint_genEigenspace, ENat.one_le_iff_ne_zero_withTop, Submodule.inf_iSup_genEigenspace, Polynomial.trailingDegree_le_of_ne_zero, FiniteMultiplicity.emultiplicity_le_of_multiplicity_le, Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, Cardinal.ofENat_le_ofENat, ENat.toENNReal_lt, Polynomial.le_trailingDegree_C_mul_X_pow, Cardinal.ofNat_lt_ofENat, MvPowerSeries.weightedOrder_mul_ge, MvPowerSeries.le_order, Set.one_le_encard_insert, Set.Nonempty.encard_pos, PowerSeries.le_order_pow_of_constantCoeff_eq_zero, MvPowerSeries.order_le, ENat.toENNReal_min, Module.End.mem_genEigenspace_top, Module.End.injOn_genEigenspace, IsDiscreteValuationRing.addVal_add, Module.End.genEigenspace_one, Set.encard_iUnion_le_of_finite, Cardinal.toENatAux_gc, AddCircle.card_torsion_le_of_isSMulRegular_int, Cardinal.toNat_toENat, ENat.toENNReal_mono, pow_dvd_iff_le_emultiplicity, ENat.epow_left_mono, Polynomial.natTrailingDegree_le_trailingDegree, PowerSeries.min_order_le_order_add, toENat_rank_span_set, Set.encard_mono, dvd_iff_emultiplicity_pos, ENat.add_lt_add_iff_left, Set.encard_singleton_inter, ENat.one_le_epow, Cardinal.toENat_strictMonoOn, Matroid.ExchangeProperty.encard_diff_le_aux, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, Cardinal.ofNat_le_ofENat, ENat.addLECancellable_coe, Submodule.spanRank_toENat_eq_iInf_finset_card, ENat.pow_lt_top_iff, Set.encard_le_coe_iff_finite_ncard_le, MvPowerSeries.le_order_smul, PowerSeries.le_order_pow, emultiplicity_prime_le_emultiplicity_image_by_factor_orderIso, squarefree_iff_emultiplicity_le_one, Cardinal.continuum_toENat, Polynomial.trailingDegree_lt_wf, Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT, Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, ENat.le_coe_iff, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, Set.encard_le_encard_iff_encard_diff_le_encard_diff, Module.End.genEigenspace_zero_nat, FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt, ENat.lt_add_one_iff, ENat.addLECancellable_of_ne_top, Cardinal.ofENat_lt_ofENat, Module.End.genEigenspace_top, Cardinal.ofENat_strictMono, Polynomial.ringKrullDim_le, Cardinal.toENat_le_iff_of_le_aleph0, ENat.coe_lt_coe, PowerSeries.order_le, emultiplicity_lt_top, Cardinal.toENat_eq_top, ENat.coe_le_coe, MvPowerSeries.weightedOrder_le, ENat.add_one_pos, Cardinal.one_lt_ofENat, Topology.CWComplex.iUnion_openCell_eq_skeleton, Topology.RelCWComplex.skeleton_monotone, Cardinal.ofENat_lt_nat, Set.encard_image_le, MvPowerSeries.weightedOrder_add_of_weightedOrder_ne, Module.End.generalized_eigenvec_disjoint_range_ker, Cardinal.ofENat_le_one, Cardinal.ofENat_pos, ENat.add_le_add_iff_right, Nat.Prime.emultiplicity_factorial_le_div_pred, UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors, Cardinal.toENat_le_natCast_iff, Set.toENat_cardinalMk, ENat.mul_left_strictMono, Module.End.mem_genEigenspace_one, Cardinal.enat_gc, PowerSeries.le_order, Set.one_lt_encard_iff, MvPowerSeries.order_mul_ge, Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace, Cardinal.toENatAux_le_nat, Cardinal.toENat_le_nat, Set.encard_pos, ENat.toENNReal_max, Module.End.genEigenspace_div, Set.encard_le_coe_iff, MvPowerSeries.le_weightedOrder, Module.End.genEigenspace_eq_genEigenspace_finrank_of_le, Set.encard_lt_encard_iff_encard_diff_lt_encard_diff, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, Module.End.genEigenspace_nat, Cardinal.toENat_comp_ofENat, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, ENat.strictMono_map_iff, ENat.one_lt_top, Module.End.genEigenspace_le_maximal, Cardinal.toENat_le_iff_of_lt_aleph0, Module.End.mem_genEigenspace_nat, Cardinal.ofENat_toENat_le, MvPowerSeries.order_add_of_order_ne, Set.encard_insert_le, Set.encard_le_one_iff, Cardinal.toENat_le_one, Set.encard_le_encard_of_injOn, Set.encard_tsub_one_le_encard_diff_singleton, ENat.mul_le_mul_right_iff, Cardinal.toENat_injOn, LinearIndepOn.encard_le_toENat_rank, Cardinal.toENat_eq_nat, Set.one_lt_encard_iff_nontrivial, min_le_emultiplicity_add, emultiplicity_pos_iff, ENat.succ_def, Cardinal.nat_le_ofENat, Cardinal.ofENat_toENat_eq_self, ENat.exists_nat_gt, Cardinal.ofENat_toENat, Function.Injective.encard_range, Set.encard_le_one_iff_eq, Topology.RelCWComplex.skeletonLT_I, Cardinal.aleph_toENat, IsDiscreteValuationRing.addVal_le_iff_dvd, Set.encard_le_encard, ENat.toENNReal_le, Cardinal.toENat_eq_iff_of_le_aleph0, PowerSeries.order_add_of_order_ne, Module.End.hasGenEigenvector_iff, ENat.tendsto_nhds_top_iff_natCast_lt, Module.End.mem_genEigenspace_zero, Set.encard_iUnion_le_of_fintype, Set.one_le_encard_iff_nonempty, Ideal.height_le_spanRank_toENat, Cardinal.natCast_eq_toENat_iff, ENat.eq_top_iff_forall_ge, Cardinal.ofENat_le_nat, ENat.mul_le_mul_left_iff, Module.End.genEigenspace_le_genEigenspace_finrank, Module.End.mem_genEigenspace, le_emultiplicity_iff_replicate_subperm_primeFactorsList, Cardinal.toENat_nat, Topology.RelCWComplex.skeletonLT_monotone, PowerSeries.nat_le_order, Module.End.genEigenspace_zero, Polynomial.le_trailingDegree_X_pow, Matroid.toENat_cRank_eq, Set.Finite.encard_biUnion_le, MvPowerSeries.le_order_pow, ENat.one_lt_card, ENat.self_le_mul_right, ENat.add_le_add_iff_left, ENat.mul_right_strictMono, Module.End.genEigenspace_le_smul, MvPowerSeries.min_order_le_add, PowerSeries.le_order_prod, PowerSeries.order_add_of_order_eq, Matrix.eRank_submatrix_le, Module.End.genEigenspace_restrict, Cardinal.natCast_le_toENat_iff, Polynomial.trailingDegree_one_le, Stream'.Seq.lt_length'_iff, Set.Finite.encard_strictMonoOn, ENat.add_lt_add_iff_right, multiplicity_le_emultiplicity, Set.encard_le_one_iff_subsingleton, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, ENat.lt_coe_add_one_iff, ENat.card_le_one, Polynomial.le_trailingDegree_X, Module.length_eq_rank, Order.krullDim_le_of_krullDim_preimage_le', Cardinal.toENat_lt_top, MvPowerSeries.le_order_pow_of_constantCoeff_eq_zero, Cardinal.toENat_congr, ENat.range_natCast, ENat.one_le_iff_ne_zero, ENat.lt_one_iff_eq_zero, Matroid.toENat_cRk_eq, Set.encard_le_encard_diff_add_encard, Cardinal.toENat_eq_one, ENat.not_lt_zero, ENat.top_mul', ENat.coe_lt_top, Cardinal.nat_lt_ofENat, WithBot.add_one_le_iff, MvPowerSeries.le_order_map
|
instLinearOrderedAddCommMonoidWithTopENat 📖 | CompOp | 27 mathmath: IsDiscreteValuationRing.addVal_zero, Finset.set_encard_biUnion_le, Finset.emultiplicity_prod, multiplicity_addValuation_apply, Set.encard_iUnion_of_finite, IsDiscreteValuationRing.addVal_def', Irreducible.addVal_pow, IsDiscreteValuationRing.addVal_uniformizer, MvPowerSeries.le_weightedOrder_subst, IsDiscreteValuationRing.addVal_mul, IsDiscreteValuationRing.addVal_add, Set.encard_iUnion_le_of_finite, IsDiscreteValuationRing.addVal_pow, IsDiscreteValuationRing.addVal_eq_zero_iff, PowerSeries.order_prod, Module.length_pi_of_fintype, IsDiscreteValuationRing.addVal_eq_top_iff, IsDiscreteValuationRing.addVal_eq_zero_of_unit, Set.Finite.encard_biUnion, IsDiscreteValuationRing.addVal_def, MvPowerSeries.order_prod, IsDiscreteValuationRing.addVal_one, IsDiscreteValuationRing.addVal_le_iff_dvd, Set.encard_iUnion_le_of_fintype, Set.Finite.encard_biUnion_le, PowerSeries.le_order_prod, MvPowerSeries.weightedOrder_prod
|
instNoZeroDivisorsENat 📖 | CompOp | 3 mathmath: Order.krullDim_le_of_krullDim_preimage_le, Polynomial.ringKrullDim_le, Order.krullDim_le_of_krullDim_preimage_le'
|
instNontrivialENat 📖 | CompOp | 3 mathmath: Order.krullDim_le_of_krullDim_preimage_le, Polynomial.ringKrullDim_le, Order.krullDim_le_of_krullDim_preimage_le'
|
instOrderBotENat 📖 | CompOp | — |
instOrderTopENat 📖 | CompOp | — |
instOrderedSubENat 📖 | CompOp | — |
instSubENat 📖 | CompOp | 37 mathmath: SimpleGraph.vertexCoverNum_le_card_sub_one, ContinuousOn.enatSub, Set.tsub_encard_le_encard_diff, ENat.le_sub_of_add_le_right, Mathlib.Tactic.ENatToNat.coe_sub, ContinuousWithinAt.enatSub, ENat.ceil_sub_one, SimpleGraph.vertexCoverNum_top, ENat.toENNReal_sub, Stream'.Seq.drop_length', ENat.top_sub_one, Continuous.enatSub, ENat.sub_eq_top_iff, ENat.continuousAt_sub, ENat.sub_iSup, ENat.floor_sub_natCast, ENat.le_sub_of_add_le_left, Order.height_eq_coe_iff, ContinuousAt.enatSub, ENat.ceil_sub_natCast, ENat.floor_sub_toENNReal, ENat.top_sub_coe, Filter.Tendsto.enatSub, ENat.coe_sub, ENat.ceil_sub_toENNReal, ENat.le_sub_one_of_lt, ENat.top_sub_ofNat, ENat.ceil_sub_ofNat, ENat.sub_top, ENat.floor_sub_ofNat, Set.encard_diff, Order.coheight_eq_coe_iff, ENat.floor_sub_one, Set.encard_tsub_one_le_encard_diff_singleton, ENat.sub_sub_cancel, ENat.toNat_sub, Set.encard_diff_singleton_of_mem
|
instSuccOrderENat 📖 | CompOp | 1 mathmath: ENat.succ_def
|
instWellFoundedLTENat 📖 | CompOp | — |
instZeroENat 📖 | CompOp | 187 mathmath: instContMDiffAddOfNatWithTopENatOfContinuousAdd, AlgebraicGeometry.Scheme.height_of_isClosed, ENat.floor_pos, ENat.top_pos, Matroid.eRk_loops, Metric.externalCoveringNumber_eq_zero, Set.encard_eq_zero, emultiplicity_of_isUnit_right, Metric.packingNumber_eq_zero, Matroid.eRk_empty, Matroid.eRank_loopyOn, SimpleGraph.chromaticNumber_pos, Order.krullDim_nonneg_iff, Dynamics.coverMincard_eq_zero_iff, ENat.iSup_zero, ENat.card_pos, instLieGroupOfNatWithTopENatOfIsTopologicalGroup, Module.length_eq_zero, Order.krullDim_pos_iff, emultiplicity_zero_eq_zero_of_ne_zero, instContMDiffInv₀OfNatWithTopENatOfContinuousInv₀, contDiff_zero, SimpleGraph.radius_eq_zero_iff, emultiplicity_of_one_right, Order.height_pos, Cardinal.toENat_eq_zero, IsManifold.instLEInftyOfNatWithTopENat_2, Order.krullDim_eq_zero_of_unique, emultiplicity_pos_of_dvd, ENat.card_eq_zero_iff_empty, Dynamics.coverMincard_empty, ENat.sSup_eq_zero, Polynomial.le_trailingDegree_C, Polynomial.trailingDegree_eq_zero, ENat.map_natCast_eq_zero, ENat.toNat_zero, Order.krullDim_nonpos_iff_forall_isMax, instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup, Module.length_eq_zero_of_subsingleton_ring, ringKrullDim_nonneg_of_nontrivial, ringKrullDimZero_iff_ringKrullDim_eq_zero, hasFTaylorSeriesUpTo_zero_iff, Order.krullDim_nonpos_iff_forall_isMin, Module.length_pos_iff, SimpleGraph.edist_self, ENat.zero_epow, Metric.coveringNumber_empty, Metric.externalCoveringNumber_empty, Matroid.eRank_emptyOn, SimpleGraph.edist_top, SimpleGraph.chromaticNumber_eq_zero_of_isEmpty, contDiffWithinAt_zero, contMDiff_zero_iff, SimpleGraph.eccent_eq_zero_iff, PartENat.toWithTop_zero', Set.encard_empty, topologicalKrullDim_zero_of_discreteTopology, ENat.sInf_eq_zero, emultiplicity_eq_zero_iff_multiplicity_eq_zero, Dynamics.netMaxcard_empty, Stream'.Seq.length'_nil, Order.coheight_pos_of_lt_top, hasFTaylorSeriesUpToOn_zero_iff, Order.height_pos_of_bot_lt, Order.IsMax.coheight_eq_zero, SimpleGraph.edist_pos_of_ne, Cardinal.ofENat_eq_zero, ENat.ceil_pos, emultiplicity_eq_zero, Order.krullDim_nonpos_of_subsingleton, Order.height_eq_zero, ENat.toENNReal_zero, Real.contDiffAt_arcsin_iff, contDiffOn_zero, SimpleGraph.vertexCoverNum_eq_zero, Matrix.eRank_zero, ENat.mul_top', ENat.lift_zero, Matroid.eRk_loopyOn, Topology.RelCWComplex.skeletonLT_zero_eq_base, Matroid.IsLoop.eRk_eq, Module.length_bot, ENat.ceil_zero, Set.Nonempty.encard_pos, AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top, contDiffGroupoid_zero_eq, SimpleGraph.edist_bot, SimpleGraph.ediam_eq_zero_of_subsingleton, Metric.coveringNumber_pos_iff, Polynomial.trailingDegree_C, PowerSeries.order_exp, Order.coheight_eq_zero, ENat.epow_eq_one_iff, dvd_iff_emultiplicity_pos, Order.coheight_top, Set.chainHeight_empty, ENat.epow_eq_zero_iff, Matroid.eRank_eq_zero_iff, Stream'.Seq.length'_eq_zero_iff_nil, SimpleGraph.eccent_pos_iff, SimpleGraph.vertexCoverNum_of_subsingleton, Order.krullDim_eq_zero_iff_of_orderTop, Module.length_pos, PartENat.toWithTop_zero, Mathlib.Tactic.ENatToNat.coe_zero, ringKrullDim_eq_zero_of_isField, Order.height_bot, ENat.iSup_eq_zero, Matroid.eRk_eq_zero_iff', ENat.recTopCoe_zero, Ideal.primeHeight_eq_zero_iff, ENat.floor_zero, emultiplicity_of_unit_right, SimpleGraph.ediam_eq_zero_iff_subsingleton, IsDiscreteValuationRing.addVal_eq_zero_iff, Matroid.eRk_eq_zero_iff, Cardinal.toENatAux_zero, AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top, SimpleGraph.chromaticNumber_eq_zero_of_isempty, PowerSeries.order_zero_of_unit, ENat.add_one_pos, PowerSeries.order_one, PartENat.withTopEquiv_symm_zero, Module.length_eq_zero_iff, instContMDiffVectorBundleOfNatWithTopENat_1, Cardinal.toENatAux_eq_zero, Polynomial.trailingDegree_one, Order.krullDim_pos_iff_of_orderTop, Cardinal.ofENat_pos, ENat.sub_top, Order.krullDim_eq_zero, Set.encard_pos, Order.krullDim_pos_iff_of_orderBot, PartENat.withTopEquiv_zero, instIsContMDiffRiemannianBundleOfNatWithTopENat, IsDiscreteValuationRing.addVal_eq_zero_of_unit, ENat.toNat_eq_zero, contDiffAt_zero, Nat.Prime.emultiplicity_one, Dynamics.netMaxcard_eq_zero_iff, SimpleGraph.vertexCoverNum_bot, instContMDiffMulOfNatWithTopENatOfContinuousMul, analyticOrderAt_of_not_analyticAt, analyticOrderAt_eq_zero, PartENat.ofENat_zero, Cardinal.zero_eq_ofENat, IsDiscreteValuationRing.addVal_one, Ring.ord_one, emultiplicity_pos_iff, Topology.CWComplex.skeletonLT_zero_eq_empty, Order.IsMin.height_eq_zero, Metric.externalCoveringNumber_pos_iff, ENat.floor_eq_zero, Order.krullDim_nonneg, Metric.coveringNumber_eq_zero, Order.coheight_pos, SimpleGraph.edist_eq_zero_iff, ringKrullDim_eq_zero_of_field, ENat.iInf_eq_zero, Metric.packingNumber_pos_iff, Module.End.mem_genEigenspace_zero, Matroid.eq_loopyOn_iff_eRank, ENat.coe_zero, ENat.sSup_eq_zero', ENat.map_zero, Metric.packingNumber_empty, Set.chainHeight_of_isEmpty, Module.End.genEigenspace_zero, Ideal.height_bot, Set.chainHeight_eq_zero_iff, Cardinal.ofENat_zero, contMDiffOn_zero_iff, ENat.zero_epow_top, ContDiffPointwiseHolderAt.zero_order_iff, Real.contDiffAt_arccos_iff, Order.krullDim_eq_zero_iff_of_orderBot, Polynomial.trailingDegree_one_le, ENat.ceil_eq_zero, Mathlib.Meta.Positivity.natCeil_pos, MvPowerSeries.weightedOrder_one, IsManifold.instOfNatWithTopENat, SimpleGraph.eccent_eq_zero_of_subsingleton, ENat.lt_one_iff_eq_zero, ENat.epow_zero, ENat.not_lt_zero, ENat.top_mul', AnalyticAt.analyticOrderAt_eq_zero
|