| Metric | Count |
|---|
DefinitionsENatMap, ENatMap, instSuccAddOrder, instUniqueUnits, instWellFoundedRelation, map, toNat, toNatHom, ENatMap, ENatMap, ENatMap, ENatMap, instAddENat, instAddMonoidWithOneENat, instBotENat, instCanonicallyOrderedAddENat, instCharZeroENat, instCommSemiringENat, instIsOrderedRingENat, instLEENat, instLTENat, instLinearOrderENat, instLinearOrderedAddCommMonoidWithTopENat, instNoZeroDivisorsENat, instNontrivialENat, instOrderBotENat, instOrderTopENat, instOrderedSubENat, instPreorderENat, instSubENat, instSuccOrderENat, instWellFoundedLTENat, instZeroLEOneClassENat | 33 |
TheoremsENatMap_apply, ENatMap_apply, add_le_add_natCast_left_iff, add_le_add_natCast_right_iff, add_le_add_one_left_iff, add_le_add_one_right_iff, add_natCast_cancel, add_ofNat_cancel, add_one_cancel, add_one_le_iff, lt_add_one_iff, natCast_add_cancel, ofNat_add_cancel, one_add_cancel, 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, add_lt_add_iff_left, add_lt_add_iff_right, add_lt_add_of_le_of_lt, add_lt_add_of_lt_of_le, 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_one_iff_eq_zero_or_eq_one, 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_coe, succ_def, succ_top, 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 | 154 |
| Total | 187 |
| Name | Category | Theorems |
|---|
instAddENat 📖 | CompOp | 244 mathmath: Order.coheight_add_one_le, ENat.add_lt_top, ENat.add_lt_add, Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ, Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, ENat.WithBot.one_add_cancel, ENat.lt_add_one_iff', ringKrullDim_succ_le_ringKrullDim_polynomial, Set.encard_diff_add_encard, Set.encard_union_eq, ContDiffMapSupportedIn.iteratedFDerivLM_apply, MvPowerSeries.le_order_mul, ENat.ceil_add_ofNat, ENat.iSup_add_iSup_of_monotone, Order.height_add_one_le, Matroid.eRank_le_encard_add_eRk_compl, ENat.floor_add_ofNat, ENat.coe_top_add_one, ENat.iInf_add_iInf, Module.supportDim_add_length_eq_supportDim_of_isRegular, ENat.ceil_add_natCast, Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown, MvPowerSeries.le_weightedOrder_mul, ENat.floor_add_one, PowerSeries.order_mul_ge, Set.encard_union_add_encard_inter, ENat.floor_add_natCast, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, ringKrullDim_succ_le_ringKrullDim_powerseries, Polynomial.height_eq_height_add_one, Nat.Prime.emultiplicity_le_emultiplicity_choose_add, contDiff_succ_iff_fderiv, ENat.biSup_add', MvPowerSeries.weightedOrder_mul, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, Topology.RelCWComplex.iUnion_openCell_eq_skeleton, Nat.two_pow_sub_pow, ENat.add_right_injective_of_ne_top, Matroid.eRk_dual_add_eRank', Nat.Prime.emultiplicity_factorial_mul, AddHom.ENatMap_apply, Order.coheight_eq_coe_add_one_iff, Matroid.eRk_le_eRk_add_eRk_diff, Set.encard_union_le, contDiffOn_succ_of_fderivWithin, emultiplicity_pow_prime_pow_sub_pow_prime_pow, Order.krullDim_le_of_krullDim_preimage_le, 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, Nat.emultiplicity_pow_add_pow, Matroid.eRk_insert_le_add_one, ENat.add_iInf, Ideal.height_le_height_add_of_liesOver, ENat.epow_add, ENat.add_iSup, Ideal.height_le_height_add_one_of_mem, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, Matroid.exists_eRk_insert_eq_add_one_of_lt, Matroid.eRk_inter_add_eRk_union_le, Module.End.genEigenspace_inf_le_add, ringKrullDim_succ_le_of_surjective, Matroid.eRk_dual_add_eRank, 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, ENat.WithBot.add_le_add_natCast_left_iff, ENat.sInf_add, contDiffOn_succ_iff_fderiv_of_isOpen, hasFTaylorSeriesUpToOn_succ_iff_right, ENat.add_sSup, Cardinal.ofENat_add, ENat.ceil_add_le, AnalyticAt.analyticOrderAt_deriv_add_one, Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors, Order.krullDim_WithTop, Matroid.eRk_insert_inter_add_eRk_insert_union_le, ringKrullDim_le_ringKrullDim_quotient_add_card, ENat.natCast_lt_succ, Ideal.height_le_ringKrullDim_quotient_add_one, analyticOrderAt_mul, Polynomial.le_trailingDegree_mul, ENat.ceil_natCast_add, Order.coheight_coe_withTop, Dynamics.coverMincard_union_le, Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ, Order.height_eq_iSup_lt_height, Order.height_eq_coe_add_one_iff, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, SimpleGraph.edist_triangle, MvPowerSeries.weightedOrder_mul_ge, ENat.card_sum, IsDiscreteValuationRing.addVal_mul, ENat.ceil_add_toENNReal, Order.coheight_le_of_krullDim_preimage_le, ringKrullDim_add_length_eq_ringKrullDim_of_isRegular, ENat.WithBot.natCast_add_cancel, 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, TestFunction.lineDerivCLM_apply, Matroid.eRk_le_eRk_inter_add_eRk_diff, ENat.iInf_add_iInf_of_monotone, Ideal.height_le_ringKrullDim_quotient_add_encard, Ideal.primeHeight_add_one_le_of_lt, tangentBundleCore.isContMDiff, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors, contDiff_succ_iff_fderiv_apply, ENat.add_one_eq_coe_top_iff, TangentBundle.contMDiffVectorBundle, Module.supportDim_quotSMulTop_succ_eq_supportDim, Matroid.IsCircuit.eRk_add_one_eq, contDiffAt_succ_iff_hasFDerivAt, ENat.add_lt_add_iff_left, Order.height_le_of_krullDim_preimage_le, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson, ENat.WithBot.add_le_add_one_left_iff, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, ENat.sSup_add, ENat.addLECancellable_coe, ENat.add_sInf, ENat.biSup_add_biSup_le', ringKrullDim_le_ringKrullDim_add_card, ENat.WithBot.add_one_cancel, Set.encard_eq_add_one_iff, ENat.toENNReal_add, ENat.iSup_add_iSup, ENat.iSup_add, Set.encard_ne_add_one, Module.supportDim_le_supportDim_quotSMulTop_succ, ENat.WithBot.add_one_le_iff, ENat.lt_add_one_iff, ENat.addLECancellable_of_ne_top, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, Module.length_prod, ENat.le_iInf_add_iInf, Matroid.eRank_add_eRank_dual, Int.emultiplicity_pow_add_pow, Polynomial.ringKrullDim_le, ENat.iInf_add, ENat.add_one_pos, ENat.WithBot.add_le_add_natCast_right_iff, Topology.CWComplex.iUnion_openCell_eq_skeleton, ENat.add_lt_add_of_le_of_lt, Int.two_pow_sub_pow, MeasureTheory.stoppedProcess_eq', Order.krullDim_withBot, Matroid.eRk_union_le_encard_add_eRk, ENat.WithBot.add_ofNat_cancel, SubAddAction.ENat_card_ofStabilizer_add_zero_eq, Matroid.eRk_union_le_eRk_add_encard, Module.length_eq_add_of_exact, ENat.add_le_add_iff_right, hasFTaylorSeriesUpToOn_succ_iff_left, Matroid.eRk_insert_eq_add_one, contDiffOn_succ_iff_fderivWithin, Order.krullDim_eq_iSup_height_add_coheight_of_nonempty, MvPowerSeries.order_mul_ge, ContDiffMapSupportedIn.fderivLM_apply, contDiffOn_succ_iff_fderiv_apply, ENat.map_add, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, ENat.floor_natCast_add, contDiff_succ_iff_deriv, contDiffOn_succ_iff_derivWithin, ENat.toNat_add, ENat.floor_toENNReal_add, ENat.WithBot.add_natCast_cancel, height_le_ringKrullDim_quotient_add_spanFinrank, ENat.floor_add_toENNReal, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, ENat.addLECancellable_of_lt_top, Ideal.height_le_height_add_encard_of_subset, Nat.Prime.emultiplicity_mul, emultiplicity_pow_prime_sub_pow_prime, analyticOrderAt_smul, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, Set.encard_insert_le, Int.two_pow_two_pow_sub_pow_two_pow, ENat.WithBot.lt_add_one_iff, Set.encard_diff_singleton_add_one, Matroid.eRk_compl_union_add_eRk_compl_inter_le, ENat.ceil_add_one, Ring.ord_mul, ContDiffMapSupportedIn.fderivCLM_apply, ENat.add_iInf₂, TestFunction.fderivCLM_apply, ENat.add_biSup, minSmoothness_add, Set.encard_diff_add_encard_inter, ringKrullDim_le_ringKrullDim_add_spanFinrank, ENat.succ_def, Set.encard_add_encard_compl, contDiffOn_succ_of_fderiv_apply, Nat.Prime.emultiplicity_factorial_mul_succ, Nat.emultiplicity_pow_sub_pow, Ideal.height_le_height_add_spanFinrank_of_le, MvPowerSeries.order_mul, ENat.add_lt_add_of_lt_of_le, Polynomial.ringKrullDim_of_isNoetherianRing, Order.height_coe_withBot, MvPolynomial.ringKrullDim_of_isNoetherianRing, Mathlib.Tactic.ENatToNat.coe_add, ENat.add_left_injective_of_ne_top, ENat.lift_add, ENat.le_iInf₂_add_iInf₂, Set.encard_insert_of_notMem, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, ENat.biSup_add_biSup_le, Polynomial.trailingDegree_mul', PowerSeries.order_mul, ENat.WithBot.ofNat_add_cancel, ENat.ceil_toENNReal_add, ENat.iSup_add_iSup_le, ENat.add_le_add_iff_left, Order.coheight_eq_iSup_gt_coheight, ENat.coe_add, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, SimpleGraph.edist_boxProd, ENat.WithBot.add_le_add_one_right_iff, ENat.ceil_le_floor_add_one, Matroid.eRk_submod, ENat.add_biSup', ENat.add_lt_add_iff_right, ENat.biSup_add, ENat.iInf₂_add, ENat.lt_coe_add_one_iff, Order.krullDim_le_of_krullDim_preimage_le', emultiplicity_mul, contDiff_succ_iff_hasFDerivAt, Set.encard_le_encard_diff_add_encard, ringKrullDim_le_ringKrullDim_quotient_add_encard, contDiffWithinAt_succ_iff_hasFDerivWithinAt, Polynomial.trailingDegree_mul
|
instAddMonoidWithOneENat 📖 | CompOp | 286 mathmath: Order.coheight_add_one_le, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ, instLieAddGroupOfNatWithTopENat, contDiffOn_nat_succ_iff_contDiffOn_one_iteratedDerivWithin, SimpleGraph.vertexCoverNum_le_card_sub_one, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, ENat.WithBot.one_add_cancel, ENat.lt_add_one_iff', ringKrullDim_succ_le_ringKrullDim_polynomial, instIsContMDiffRiemannianBundleOfNatWithTopENat_1, ENat.toNat_one, ENat.coe_one, LinearMap.IsSymmetric.diagonalization_apply_self_apply, Matroid.eRk_singleton_le, ringKrullDim_eq_one_iff_of_isLocalRing_isDomain, Cardinal.one_eq_ofENat, PowerSeries.order_expand, Order.height_add_one_le, ENat.one_lt_card_iff_nontrivial, ENat.map_one, ENat.coe_top_add_one, Order.krullDim_le_one_iff, Dynamics.coverMincard_univ, contDiff_one_iff_fderiv, contMDiff_equivTangentBundleProd_symm, contDiff_nat_succ_iff_contDiff_one_iteratedDeriv, LinearMap.IsSymmetric.directSum_decompose_apply, ENat.floor_add_one, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, Matroid.IsNonloop.eRk_eq, ringKrullDim_succ_le_ringKrullDim_powerseries, Polynomial.height_eq_height_add_one, Dynamics.one_le_coverMincard_iff, ENat.ceil_sub_one, contDiff_succ_iff_fderiv, FiniteMultiplicity.emultiplicity_self, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, Topology.RelCWComplex.iUnion_openCell_eq_skeleton, Dynamics.netMaxcard_zero, Nat.two_pow_sub_pow, ENat.one_le_card_iff_nonempty, contDiffAt_one_iff, Order.coheight_eq_coe_add_one_iff, contDiffOn_one_iff_derivWithin, ENat.card_le_one_iff_subsingleton, Metric.externalCoveringNumber_le_one_of_ediam_le, SimpleGraph.eccent_le_one_iff, ENat.lift_one, contDiffOn_succ_of_fderivWithin, IsPrincipalIdealRing.height_eq_one_of_isMaximal, Order.krullDim_le_of_krullDim_preimage_le, ENat.add_one_le_iff, Stream'.Seq.length'_cons, SimpleGraph.edist_top, MvPowerSeries.one_le_order_iff_constCoeff_eq_zero, SimpleGraph.vertexCoverNum_top, Matroid.eRk_insert_le_add_one, MvPowerSeries.le_weightedOrder_pow, Module.End.hasUnifEigenvalue_iff_mem_spectrum, Ideal.height_le_height_add_one_of_mem, ContDiff.norm_rpow, 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, ringKrullDim_succ_le_of_surjective, ENat.top_sub_one, Cardinal.one_le_ofENat, instContMDiffInv₀OfNatWithTopENat, Metric.coveringNumber_eq_one_of_ediam_le, SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable, Topology.RelCWComplex.openCell_subset_skeletonLT, Topology.RelCWComplex.closedCell_subset_skeletonLT, contDiffOn_succ_iff_fderiv_of_isOpen, hasFTaylorSeriesUpToOn_succ_iff_right, IsDiscreteValuationRing.addVal_uniformizer, instIsManifoldMinSmoothnessOfNatWithTopENat_1, AnalyticAt.analyticOrderAt_deriv_add_one, Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors, Order.krullDim_WithTop, Dynamics.coverMincard_zero, ENat.natCast_lt_succ, PowerSeries.one_le_order_iff_constCoeff_eq_zero, Ideal.height_le_ringKrullDim_quotient_add_one, instContMDiffVectorBundleOfNatWithTopENat, SimpleGraph.ediam_top, Order.coheight_coe_withTop, Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ, 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, contDiffWithinAt_succ_iff_hasFDerivWithinAt', contDiffOn_succ_iff_hasFDerivWithinAt, Order.height_eq_coe_iff, LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot', SimpleGraph.ediam_eq_one, AddMonoidHom.ENatMap_apply, ENat.floor_one, Matrix.eRank_subsingleton, Set.one_le_encard_insert, IsManifold.instLEInftyOfNatWithTopENat_1, Nat.Prime.emultiplicity_self, Module.length_eq_one, Metric.externalCoveringNumber_eq_one_of_ediam_le, ENat.epow_one, Module.End.genEigenspace_one, Order.coheight_le_of_krullDim_preimage_le, Order.krullDim_le_one_iff_of_boundedOrder, SubMulAction.ENat_card_ofStabilizer_add_one_eq, contDiffOn_succ_iff_deriv_of_isOpen, TestFunction.lineDerivCLM_apply, instContMDiffMulOfNatWithTopENat, Manifold.riemannianEDist_def, Ideal.primeHeight_add_one_le_of_lt, Set.one_le_chainHeight_iff, tangentBundleCore.isContMDiff, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors, 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, contDiffAt_succ_iff_hasFDerivAt, ENat.epow_eq_one_iff, Set.encard_singleton_inter, Order.height_le_of_krullDim_preimage_le, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson, Module.length_eq_one_iff, ENat.one_le_epow, LinearMap.IsSymmetric.direct_sum_isInternal, Matroid.eRk_eq_one_iff, ENat.WithBot.add_le_add_one_left_iff, Metric.externalCoveringNumber_singleton, IsPrincipalIdealRing.ringKrullDim_eq_one, IsDiscreteValuationRing.addVal_pow, Set.encard_lt_one, ENat.epow_def, PowerSeries.le_order_pow, analyticOrderAt_pow, Order.one_le_krullDim_iff, squarefree_iff_emultiplicity_le_one, Set.encard_eq_one, ENat.toENNReal_one, ENat.WithBot.add_one_cancel, analyticOrderAt_id, Set.encard_eq_add_one_iff, PowerSeries.order_pow, SimpleGraph.chromaticNumber_le_one_of_subsingleton, MvPowerSeries.order_expand, ENat.recTopCoe_one, Set.encard_ne_add_one, Module.supportDim_le_supportDim_quotSMulTop_succ, ENat.WithBot.add_one_le_iff, ENat.lt_add_one_iff, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, Module.End.HasUnifEigenvalue.pow, Cardinal.toENat_lt_one, Polynomial.ringKrullDim_le, ENat.le_sub_one_of_lt, differentiableWithinAt_localInvariantProp, ContDiffOn.one_of_succ, 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, ContDiff.one_of_succ, Ideal.map_height_le_one_of_mem_minimalPrimes, contDiff_one_iff_hasFDerivAt, Int.two_pow_sub_pow, MeasureTheory.stoppedProcess_eq', Order.krullDim_le_one_iff_forall_isMax, Order.krullDim_withBot, Cardinal.ofENat_le_one, Metric.packingNumber_singleton, contMDiff_equivTangentBundleProd, instIsManifoldOfNatWithTopENatOfMinSmoothness_1, SubAddAction.ENat_card_ofStabilizer_add_zero_eq, Module.End.mem_genEigenspace_one, hasFTaylorSeriesUpToOn_succ_iff_left, Matroid.eRk_insert_eq_add_one, contDiffOn_succ_iff_fderivWithin, Set.one_lt_encard_iff, ContDiffMapSupportedIn.fderivLM_apply, Module.End.genEigenspace_div, contDiffOn_succ_iff_fderiv_apply, AnalyticAt.analyticOrderAt_eq_one_of_zero_deriv_ne_zero, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, contDiff_succ_iff_deriv, IsManifold.instOfNatWithTopENat_1, Module.End.HasUnifEigenvalue.of_mem_spectrum, contDiffOn_succ_iff_derivWithin, ENat.card_eq_one_iff_unique, Dynamics.netMaxcard_univ, ENat.le_one_iff_eq_zero_or_eq_one, Module.End.Eigenvalues.val_mk, PowerSeries.coe_orderHom, instContMDiffAddOfNatWithTopENat, Matroid.eRk_singleton_eq, Order.coheight_eq_coe_iff, contDiffOn_succ_iff_hasFDerivWithinAt_of_uniqueDiffOn, ENat.one_lt_top, ENat.floor_sub_one, emultiplicity_pow_prime_sub_pow_prime, Set.encard_insert_le, SimpleGraph.radius_top, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing, ENat.WithBot.lt_add_one_iff, Set.encard_le_one_iff, Cardinal.toENat_le_one, Set.encard_diff_singleton_add_one, Set.encard_tsub_one_le_encard_diff_singleton, ENat.ceil_add_one, Set.one_lt_encard_iff_nontrivial, ContDiffMapSupportedIn.fderivCLM_apply, TestFunction.fderivCLM_apply, ENat.succ_def, PowerSeries.order_X, Order.krullDim_eq_one_iff_of_boundedOrder, Set.encard_le_one_iff_eq, Matroid.eRk_le_one_iff, Cardinal.one_le_toENat, 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, contDiff_norm_rpow, Order.krullDim_le_one_iff_forall_isMin, Polynomial.ringKrullDim_of_isNoetherianRing, Order.height_coe_withBot, Set.one_le_encard_iff_nonempty, Set.encard_insert_of_notMem, Metric.coveringNumber_singleton, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, Matroid.one_le_eRank, Set.encard_diff_singleton_of_mem, Cardinal.one_lt_toENat, exists_continuousLinearEquiv_fderiv_symm_eq, MvPowerSeries.le_order_pow, Manifold.exists_lt_of_riemannianEDist_lt, ENat.one_lt_card, Order.coheight_eq_iSup_gt_coheight, AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero, exists_continuousLinearEquiv_fderivWithin_symm_eq, SimpleGraph.edist_top_of_ne, Order.krullDim_of_isSimpleOrder, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, Mathlib.Tactic.ENatToNat.coe_one, Cardinal.ofENat_one, ENat.WithBot.add_le_add_one_right_iff, ENat.ceil_le_floor_add_one, SimpleGraph.chromaticNumber_eq_one_iff, Dynamics.one_le_netMaxcard_iff, Manifold.exists_lt_locally_constant_of_riemannianEDist_lt, SimpleGraph.edist_eq_one_iff_adj, Set.encard_le_one_iff_subsingleton, Set.encard_singleton, ENat.lt_coe_add_one_iff, ENat.card_le_one, Polynomial.le_trailingDegree_X, Order.krullDim_le_of_krullDim_preimage_le', instLieGroupOfNatWithTopENat, Order.one_lt_height_iff, Polynomial.trailingDegree_X, Polynomial.emultiplicity_le_one_of_separable, ENat.one_le_iff_ne_zero, contDiff_succ_iff_hasFDerivAt, Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one, ENat.lt_one_iff_eq_zero, contDiff_one_iff_deriv, Cardinal.toENat_eq_one, ENat.epow_zero, contDiffWithinAt_succ_iff_hasFDerivWithinAt, ENat.one_epow, SimpleGraph.eccent_top, SimpleGraph.chromaticNumber_bot, SimpleGraph.edist_le_one_iff_adj_or_eq, Metric.coveringNumber_le_one_of_ediam_le, LinearMap.IsSymmetric.eigenvectorBasis_def
|
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 | 309 mathmath: instContMDiffAddOfNatWithTopENatOfContinuousAdd, Cardinal.natCast_lt_toENat_iff, AlgebraicGeometry.Scheme.height_of_isClosed, ENat.floor_pos, ENat.top_pos, Matroid.eRk_loops, Metric.externalCoveringNumber_eq_zero, Set.encard_eq_zero, Set.toENat_cardinalMk_subtype, ENat.self_le_mul_left, emultiplicity_of_isUnit_right, Cardinal.toENat_eq_natCast_iff, Metric.packingNumber_eq_zero, Matroid.eRk_empty, ENat.card_prod, ENat.iInf_mul_of_ne, Set.encard_prod, Matroid.eRank_loopyOn, Cardinal.toENat_ofENat, SimpleGraph.chromaticNumber_pos, Order.krullDim_nonneg_iff, Dynamics.coverMincard_eq_zero_iff, Module.length_of_free, 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, Submodule.spanRank_toENat_eq_iInf_encard, SimpleGraph.radius_eq_zero_iff, emultiplicity_of_one_right, Order.height_pos, Cardinal.toENat_eq_zero, IsManifold.instLEInftyOfNatWithTopENat_2, MvPowerSeries.le_order_prod, Order.krullDim_eq_zero_of_unique, Cardinal.toENat_eq_ofNat, emultiplicity_pos_of_dvd, ENat.card_eq_zero_iff_empty, Dynamics.coverMincard_empty, ENat.mul_iSup, ENat.sSup_eq_zero, Polynomial.le_trailingDegree_C, Polynomial.trailingDegree_eq_zero, MvPowerSeries.le_weightedOrder_prod, ENat.map_natCast_eq_zero, ENat.toNat_zero, ENat.epow_natCast, Order.krullDim_nonpos_iff_forall_isMax, instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup, Module.length_eq_zero_of_subsingleton_ring, ENat.iInf_mul', 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, Mathlib.Tactic.ENatToNat.coe_mul, Cardinal.toENat_lt_natCast_iff, ENat.zero_epow, Cardinal.ofNat_eq_toENat, Metric.coveringNumber_empty, Metric.externalCoveringNumber_empty, Matroid.eRank_emptyOn, ENat.epow_mul, Order.krullDim_le_of_krullDim_preimage_le, Cardinal.toENat_lift, SimpleGraph.edist_top, SimpleGraph.chromaticNumber_eq_zero_of_isEmpty, ENat.iInf_mul, Cardinal.toENat_le_ofNat, contDiffWithinAt_zero, ENat.epow_add, MvPowerSeries.le_order_subst, contMDiff_zero_iff, SimpleGraph.eccent_eq_zero_iff, ENat.mul_sSup, Set.encard_empty, Cardinal.natCast_lt_toENat, topologicalKrullDim_zero_of_discreteTopology, ENat.sInf_eq_zero, ENat.instContinuousMul, emultiplicity_eq_zero_iff_multiplicity_eq_zero, Dynamics.netMaxcard_empty, Stream'.Seq.length'_nil, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, Order.coheight_pos_of_lt_top, RingHom.ENatMap_apply, hasFTaylorSeriesUpToOn_zero_iff, Order.height_pos_of_bot_lt, Order.IsMax.coheight_eq_zero, SimpleGraph.edist_pos_of_ne, Cardinal.toENat_lt_natCast, ENat.mul_le_mul_of_le_right, Cardinal.ofENat_eq_zero, ENat.ceil_pos, ENat.map_natCast_mul, emultiplicity_eq_zero, Order.krullDim_nonpos_of_subsingleton, Order.height_eq_zero, ENat.coe_mul, ENat.prod_lt_top, Cardinal.toENat_ofNat, ENat.toENNRealRingHom_apply, ENat.toENNReal_zero, Real.contDiffAt_arcsin_iff, contDiffOn_zero, SimpleGraph.vertexCoverNum_eq_zero, ENat.coe_toNatHom, Matrix.eRank_zero, ENat.mul_top', ENat.lift_zero, Cardinal.ofENat_mul, Matroid.eRk_loopyOn, Topology.RelCWComplex.skeletonLT_zero_eq_base, Matroid.IsLoop.eRk_eq, Module.length_bot, ENat.ceil_zero, Set.Nonempty.encard_pos, ENat.toNatHom_apply, ENat.mul_iInf_of_ne, ENat.mul_epow, AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top, Order.coheight_le_of_krullDim_preimage_le, contDiffGroupoid_zero_eq, SimpleGraph.edist_bot, Cardinal.toNat_toENat, SimpleGraph.ediam_eq_zero_of_subsingleton, Cardinal.natCast_le_toENat, Metric.coveringNumber_pos_iff, Polynomial.trailingDegree_C, PowerSeries.order_exp, SimpleGraph.ediam_le_two_mul_radius, Order.coheight_eq_zero, toENat_rank_span_set, ENat.epow_eq_one_iff, ENat.iSup_mul, Cardinal.toENat_lt_ofNat, dvd_iff_emultiplicity_pos, Cardinal.toENat_le_natCast, Dynamics.coverMincard_le_pow, Order.height_le_of_krullDim_preimage_le, Dynamics.coverMincard_mul_le_pow, Order.coheight_top, Set.chainHeight_empty, ENat.epow_eq_zero_iff, Matroid.eRank_eq_zero_iff, Stream'.Seq.length'_eq_zero_iff_nil, Cardinal.toENat_strictMonoOn, ENat.toNat_mul, SimpleGraph.eccent_pos_iff, SimpleGraph.vertexCoverNum_of_subsingleton, Order.krullDim_eq_zero_iff_of_orderTop, Module.length_pos, Submodule.spanRank_toENat_eq_iInf_finset_card, SimpleGraph.ediam_le_two_mul_eccent, ENat.pow_lt_top_iff, ENat.epow_def, Module.length_finsupp, Mathlib.Tactic.ENatToNat.coe_zero, ringKrullDim_eq_zero_of_isField, Order.height_bot, ENat.iSup_eq_zero, Matroid.eRk_eq_zero_iff', Cardinal.continuum_toENat, 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, AnalyticAt.analyticOrderAt_comp, Matroid.eRk_eq_zero_iff, PowerSeries.le_order_subst, ENat.pow_eq_top_iff, Cardinal.toENat_lt_one, Cardinal.toENatAux_zero, AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top, Polynomial.ringKrullDim_le, ENat.mul_iInf, Cardinal.toENat_le_iff_of_le_aleph0, ENat.sSup_mul, Cardinal.toENat_eq_top, Cardinal.ofNat_le_toENat, PowerSeries.order_zero_of_unit, ENat.add_one_pos, PowerSeries.order_one, Module.length_eq_zero_iff, instContMDiffVectorBundleOfNatWithTopENat_1, Cardinal.toENatAux_eq_zero, Polynomial.trailingDegree_one, Order.krullDim_pos_iff_of_orderTop, Nat.Prime.emultiplicity_pow, Cardinal.ofENat_pos, ENat.sub_top, ENat.toENNReal_mul, Cardinal.toENat_le_natCast_iff, Set.toENat_cardinalMk, ENat.mul_left_strictMono, Cardinal.enat_gc, Order.krullDim_eq_zero, Cardinal.toENat_le_nat, Set.encard_pos, Order.krullDim_pos_iff_of_orderBot, Cardinal.toENat_eq_natCast, instIsContMDiffRiemannianBundleOfNatWithTopENat, ENat.toENNReal_pow, IsDiscreteValuationRing.addVal_eq_zero_of_unit, ENat.toNat_eq_zero, contDiffAt_zero, Set.encard_pi_eq_prod_encard, Nat.Prime.emultiplicity_one, Dynamics.netMaxcard_eq_zero_iff, ENat.le_one_iff_eq_zero_or_eq_one, SimpleGraph.vertexCoverNum_bot, instContMDiffMulOfNatWithTopENatOfContinuousMul, Cardinal.toENat_comp_ofENat, ENat.top_pow, Cardinal.toENat_le_iff_of_lt_aleph0, ENat.top_mul, analyticOrderAt_of_not_analyticAt, Cardinal.ofENat_toENat_le, analyticOrderAt_eq_zero, emultiplicity_eq_zero_of_irreducible_ne, Cardinal.toENat_le_one, emultiplicity_pow, ENat.mul_le_mul_right_iff, ENat.toNat_prod, Cardinal.zero_eq_ofENat, Cardinal.toENat_injOn, LinearIndepOn.encard_le_toENat_rank, Cardinal.toENat_eq_nat, Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne, IsDiscreteValuationRing.addVal_one, Ring.ord_one, emultiplicity_pos_iff, Cardinal.ofENat_toENat_eq_self, Topology.CWComplex.skeletonLT_zero_eq_empty, Order.IsMin.height_eq_zero, Metric.externalCoveringNumber_pos_iff, ENat.mul_iInf', Cardinal.ofENat_toENat, Module.length_pi, Cardinal.aleph_toENat, ENat.floor_eq_zero, Cardinal.one_le_toENat, Order.krullDim_nonneg, Metric.coveringNumber_eq_zero, ENat.card_pos_iff_nonempty, Order.coheight_pos, SimpleGraph.edist_eq_zero_iff, ringKrullDim_eq_zero_of_field, ENat.iInf_eq_zero, Metric.packingNumber_pos_iff, Cardinal.toENat_eq_iff_of_le_aleph0, Module.End.mem_genEigenspace_zero, Ideal.height_le_spanRank_toENat, Matroid.eq_loopyOn_iff_eRank, ENat.mul_top, Cardinal.natCast_eq_toENat_iff, ENat.coe_zero, Module.length_of_free_of_finite, ENat.sSup_eq_zero', ENat.map_zero, Metric.packingNumber_empty, ENat.mul_le_mul_left_iff, Set.chainHeight_of_isEmpty, Cardinal.toENat_nat, Cardinal.one_lt_toENat, Module.End.genEigenspace_zero, Matroid.toENat_cRank_eq, Ideal.height_bot, Set.chainHeight_eq_zero_iff, ENat.self_le_mul_right, Cardinal.ofENat_zero, ENat.mul_right_strictMono, contMDiffOn_zero_iff, ENat.zero_epow_top, ContDiffPointwiseHolderAt.zero_order_iff, Real.contDiffAt_arccos_iff, Cardinal.ofNat_lt_toENat, Order.krullDim_eq_zero_iff_of_orderBot, Cardinal.natCast_le_toENat_iff, Polynomial.trailingDegree_one_le, ENat.ceil_eq_zero, Mathlib.Meta.Positivity.natCeil_pos, PowerSeries.le_weightedOrder_subst, MvPowerSeries.weightedOrder_one, Module.length_eq_rank, Order.krullDim_le_of_krullDim_preimage_le', Cardinal.toENat_lt_top, IsManifold.instOfNatWithTopENat, MonoidWithZeroHom.ENatMap_apply, Cardinal.toENat_congr, SimpleGraph.eccent_eq_zero_of_subsingleton, ContDiffMapSupportedIn.structureMapLM_eq, ENat.lt_one_iff_eq_zero, Matroid.toENat_cRk_eq, Cardinal.toENat_eq_one, ENat.epow_zero, ENat.not_lt_zero, ENat.top_mul', Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul, Cardinal.natCast_eq_toENat, AnalyticAt.analyticOrderAt_eq_zero
|
instIsOrderedRingENat 📖 | CompOp | — |
instLEENat 📖 | CompOp | 363 mathmath: Function.Embedding.encard_le, Order.coheight_add_one_le, emultiplicity_le_emultiplicity_of_dvd_left, SimpleGraph.ediam_le_iff, SimpleGraph.ediam_anti, SimpleGraph.vertexCoverNum_le_card_sub_one, Ideal.height_le_spanFinrank, ENat.lt_add_one_iff', ENat.self_le_mul_left, ENat.card_le_card_of_injective, PowerSeries.le_order_subst_left', Topology.CWComplex.exists_mem_openCell_of_mem_skeleton, Ideal.height_le_iff_exists_minimalPrimes, SimpleGraph.le_chromaticNumber_iff_colorable, ContDiffMapSupportedIn.iteratedFDerivLM_apply, SimpleGraph.le_chromaticNumber_iff_coloring, Set.tsub_encard_le_encard_diff, Matrix.eRank_le_card_width, AddCircle.card_torsion_le_of_isSMulRegular, ENat.le_sub_of_add_le_right, MvPowerSeries.le_order_mul, Cardinal.ofENat_le_ofNat, Set.ncard_le_encard, ContDiffMapSupportedIn.structureMapCLM_apply, Matroid.eRk_singleton_le, Matrix.eRank_le_card_height, Order.coheight_le, ENat.ceil_le_ceil, Order.length_le_coheight, Dynamics.netMaxcard_le_coverMincard, Order.height_add_one_le, Finset.set_encard_biUnion_le, exists_spanRank_le_and_le_height_of_le_height, Set.encard_preimage_val_le_encard_left, SimpleGraph.Walk.edist_le, Matroid.eRank_le_encard_add_eRk_compl, SimpleGraph.vertexCoverNum_le_iff, Dynamics.coverMincard_image_le, Set.chainHeight_le_encard, Module.End.genEigenspace_directed, Matroid.le_eRk_iff, Ideal.primeHeight_mono, ENat.le_floor, Topology.RelCWComplex.mem_skeleton_iff, AddMonoid.minOrder_le_addOrderOf, Nat.count_le_setENCard, MvPowerSeries.le_weightedOrder_mul, SimpleGraph.two_le_chromaticNumber_of_adj, SimpleGraph.card_le_chromaticNumber_iff_forall_surjective, ContDiffMapSupportedIn.monoLM_apply, MvPowerSeries.le_order_prod, SimpleGraph.three_le_egirth, Dynamics.IsDynNetIn.card_le_netMaxcard, emultiplicity_le_emultiplicity_of_dvd_right, PowerSeries.order_mul_ge, SimpleGraph.chromaticNumber_le_sum_right, ENat.forall_natCast_le_iff_le, Set.encard_preimage_val_le_encard_right, Metric.coveringNumber_two_mul_le_externalCoveringNumber, PowerSeries.le_order_smul, Polynomial.le_trailingDegree_C, MvPowerSeries.le_weightedOrder_prod, Dynamics.one_le_coverMincard_iff, Nat.Prime.emultiplicity_le_emultiplicity_choose_add, SimpleGraph.chromaticNumber_le_of_forall_imp, PowerSeries.le_order_subst_right', MvPowerSeries.le_weightedOrder_map, le_emultiplicity_map, Stream'.Seq.length'_le_iff, MvPowerSeries.nat_le_order, ENat.one_le_card_iff_nonempty, Order.coheight_eq_coe_add_one_iff, SimpleGraph.vertexCoverNum_le_vertexCoverNum_of_injective, Monoid.minOrder_le_natCard, AddMonoid.le_minOrder, ENat.card_le_one_iff_subsingleton, Polynomial.le_trailingDegree_monomial, Metric.externalCoveringNumber_le_one_of_ediam_le, SimpleGraph.eccent_le_one_iff, Matroid.eRk_le_eRk_add_eRk_diff, ENat.floor_le_ceil, Dynamics.coverMincard_closure_le, MvPowerSeries.nat_le_weightedOrder, Set.encard_union_le, Polynomial.trailingDegree_le_trailingDegree, Matroid.eRk_compl_insert_union_add_eRk_compl_insert_inter_le, ENat.add_one_le_iff, MvPowerSeries.one_le_order_iff_constCoeff_eq_zero, Metric.externalCoveringNumber_anti, Cardinal.toENat_le_ofNat, Matroid.eRk_insert_le_add_one, Set.chainHeight_mono, Ideal.height_le_height_add_of_liesOver, MvPowerSeries.le_order_subst, MvPowerSeries.le_weightedOrder_pow, le_emultiplicity_of_le_multiplicity, Ideal.height_le_height_add_one_of_mem, PowerSeries.le_order_map, Matroid.spanning_iff_eRk_le', Metric.packingNumber_two_mul_le_externalCoveringNumber, emultiplicity_le_emultiplicity_iff, MvPowerSeries.min_weightedOrder_le_add, Ideal.height_le_card_of_mem_minimalPrimes_span, SimpleGraph.chromaticNumber_le_card, Matroid.eRk_inter_add_eRk_union_le, ENat.coe_toNat_le_self, SimpleGraph.vertexCoverNum_mono, Dynamics.IsDynCoverOf.coverMincard_le_card, Metric.externalCoveringNumber_mono_set, Cardinal.one_le_ofENat, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, Metric.IsCover.externalCoveringNumber_le_encard, Order.coheight_eq_coe_iff_maximal_le_coheight, ENat.ceil_le, SimpleGraph.chromaticNumber_le_iff_colorable, PowerSeries.le_order_mul, Set.encard_le_card, ENat.mul_le_mul_of_le_right, natCast_le_analyticOrderAt, ContDiffMapSupportedIn.monoCLM_apply, SimpleGraph.vertexCoverNum_le_encard_edgeSet, Matroid.Indep.encard_le_eRk_of_subset, Matroid.eRank_le_encard_ground, ENat.ceil_add_le, Matroid.eRk_insert_inter_add_eRk_insert_union_le, Ideal.height_mono, Submodule.spanFinrank_span_le_encard, Matroid.Indep.encard_le_eRank, PowerSeries.one_le_order_iff_constCoeff_eq_zero, Metric.IsCover.coveringNumber_le_encard, ENat.toENNRealOrderEmbedding_apply, le_emultiplicity_of_pow_dvd, MvPowerSeries.le_weightedOrder_smul, Ideal.height_le_iff, SimpleGraph.chromaticNumber_le_two_iff_isBipartite, Polynomial.le_trailingDegree_mul, SimpleGraph.two_le_chromaticNumber_iff_ne_bot, MvPowerSeries.le_weightedOrder_subst, Dynamics.coverMincard_union_le, MeasureTheory.stoppedProcess_eq, Stream'.Seq.at_least_as_long_as_coind, Module.length_le_of_surjective, Order.height_eq_coe_add_one_iff, Polynomial.trailingDegree_le_of_ne_zero, FiniteMultiplicity.emultiplicity_le_of_multiplicity_le, Matroid.eRk_le_iff, SimpleGraph.le_chromaticNumber_iff_forall_surjective, Order.height_le_coe_iff, ENat.le_sub_of_add_le_left, Cardinal.ofENat_le_ofENat, Polynomial.le_trailingDegree_C_mul_X_pow, SimpleGraph.edist_le_eccent, SimpleGraph.Colorable.chromaticNumber_le, SimpleGraph.edist_triangle, ENat.lift_le_iff, MvPowerSeries.weightedOrder_mul_ge, MvPowerSeries.le_order, Set.one_le_encard_insert, PowerSeries.le_order_pow_of_constantCoeff_eq_zero, Order.length_le_height, MvPowerSeries.order_le, SimpleGraph.IsVertexCover.vertexCoverNum_le, IsDiscreteValuationRing.addVal_add, Order.height_le_height_apply_of_strictMono, Set.encard_iUnion_le_of_finite, Order.coheight_le_of_krullDim_preimage_le, Matroid.eRk_union_le_eRk_add_eRk, TestFunction.lineDerivCLM_apply, Matroid.eRk_le_eRk_inter_add_eRk_diff, AddCircle.card_torsion_le_of_isSMulRegular_int, Cardinal.natCast_le_toENat, MeasureTheory.stoppedValue_sub_eq_sum', Ideal.primeHeight_add_one_le_of_lt, Set.one_le_chainHeight_iff, pow_dvd_iff_le_emultiplicity, SimpleGraph.cliqueNum_le_chromaticNumber, Polynomial.natTrailingDegree_le_trailingDegree, ENat.le_ceil, PowerSeries.min_order_le_order_add, SimpleGraph.ediam_le_two_mul_radius, Set.encard_singleton_inter, Cardinal.toENat_le_natCast, Dynamics.coverMincard_le_pow, Order.height_le_of_krullDim_preimage_le, Ideal.height_le_iff_covBy, SimpleGraph.eccent_le_ediam, Dynamics.coverMincard_mul_le_pow, le_analyticOrderAt_sub, le_analyticOrderAt_add, ENat.one_le_epow, AddMonoid.le_minOrder_iff_forall_addSubgroup, Order.height_le, Matroid.ExchangeProperty.encard_diff_le_aux, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, Order.coheight_le_coheight_apply_of_strictMono, Cardinal.ofNat_le_ofENat, ENat.addLECancellable_coe, SimpleGraph.edist_anti, SimpleGraph.ediam_le_two_mul_eccent, 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, Metric.coveringNumber_subset_le, Order.coheight_le_iff', ENat.biSup_add_biSup_le', SimpleGraph.chromaticNumber_le_one_of_subsingleton, Metric.coveringNumber_le_packingNumber, ENat.le_coe_iff, Monoid.le_minOrder_iff_forall_subgroup, Set.encard_le_encard_iff_encard_diff_le_encard_diff, Module.length_le_of_injective, SimpleGraph.IsTree.chromaticNumber_le_two, Matroid.eRk_le_eRank, ENat.lt_add_one_iff, ENat.addLECancellable_of_ne_top, ENat.le_iInf_add_iInf, SimpleGraph.le_chromaticNumber_of_pairwise_adj, PowerSeries.le_order_subst, SimpleGraph.chromaticNumber_mono, Cardinal.toENat_le_iff_of_le_aleph0, PowerSeries.order_le, ENat.le_sub_one_of_lt, Cardinal.ofNat_le_toENat, ENat.coe_le_coe, MvPowerSeries.weightedOrder_le, SimpleGraph.edist_le_ediam, Order.coheight_le_coe_iff, SimpleGraph.ediam_le_of_edist_le, Ideal.map_height_le_one_of_mem_minimalPrimes, MeasureTheory.stoppedProcess_eq', Set.encard_image_le, Matroid.eRk_union_le_encard_add_eRk, Cardinal.ofENat_le_one, SimpleGraph.radius_le_ediam, Matroid.eRk_union_le_eRk_add_encard, 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, cauchy_davenport_minOrder_add, Dynamics.coverMincard_le_netMaxcard, PowerSeries.le_order, SimpleGraph.eccent_le_iff, MvPowerSeries.order_mul_ge, ContDiffMapSupportedIn.fderivLM_apply, Cardinal.toENatAux_le_nat, Cardinal.toENat_le_nat, SimpleGraph.egirth_le_length, Set.encard_le_coe_iff, MvPowerSeries.le_weightedOrder, SimpleGraph.chromaticNumber_le_sum_left, SimpleGraph.IsClique.card_le_chromaticNumber, Set.encard_le_chainHeight_of_isChain, ENat.le_one_iff_eq_zero_or_eq_one, TestFunction.monoCLM_apply, SimpleGraph.radius_le_eccent, ENat.addLECancellable_of_lt_top, Cardinal.toENat_le_iff_of_lt_aleph0, Ideal.height_le_height_add_encard_of_subset, Metric.externalCoveringNumber_le_encard_self, Set.encard_insert_le, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing, Set.encard_le_one_iff, Order.height_le_iff, Cardinal.toENat_le_one, PowerSeries.le_order_subst_right, Metric.IsSeparated.encard_le_packingNumber, Set.encard_le_encard_of_injOn, Set.encard_tsub_one_le_encard_diff_singleton, ENat.mul_le_mul_right_iff, LinearIndepOn.encard_le_toENat_rank, Matroid.eRk_compl_union_add_eRk_compl_inter_le, ContDiffMapSupportedIn.fderivCLM_apply, TestFunction.fderivCLM_apply, min_le_emultiplicity_add, Cardinal.nat_le_ofENat, Function.Injective.encard_range, Set.encard_le_one_iff_eq, Matroid.eRk_le_one_iff, Order.height_le_iff', Cardinal.one_le_toENat, ENat.exists_le_of_sum_le, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes, IsDiscreteValuationRing.addVal_le_iff_dvd, Ideal.height_le_height_add_spanFinrank_of_le, Set.encard_le_encard, ENat.toENNReal_le, Metric.externalCoveringNumber_le_coveringNumber, Order.index_le_height, SimpleGraph.le_egirth, Metric.encard_le_of_isSeparated, Matroid.eRk_le_encard, ENat.floor_le_floor, SimpleGraph.edist_le, ENat.le_lift_iff, Set.encard_iUnion_le_of_fintype, Monoid.le_minOrder, Set.one_le_encard_iff_nonempty, Ideal.height_le_spanRank_toENat, Order.rev_index_le_coheight, cauchy_davenport_minOrder_mul, ENat.eq_top_iff_forall_ge, Cardinal.ofENat_le_nat, ENat.le_iInf₂_add_iInf₂, ENat.mul_le_mul_left_iff, Module.End.mem_genEigenspace, le_emultiplicity_iff_replicate_subperm_primeFactorsList, Matroid.one_le_eRank, ENat.biSup_add_biSup_le, Ideal.height_le_card_of_mem_minimalPrimes_span_finset, MvPowerSeries.le_weightedOrder_subst_of_forall_ne_zero, Metric.coveringNumber_le_encard_self, PowerSeries.nat_le_order, SimpleGraph.IsContained.vertexCoverNum_le_vertexCoverNum, Polynomial.le_trailingDegree_X_pow, ENat.iSup_add_iSup_le, Set.Finite.encard_biUnion_le, MvPowerSeries.le_order_pow, Set.ecard_le_ecard, ENat.self_le_mul_right, ENat.add_le_add_iff_left, Order.length_le_height_last, SimpleGraph.Walk.three_le_chromaticNumber_of_odd_loop, Metric.packingNumber_le_encard_self, MvPowerSeries.min_order_le_add, PowerSeries.le_order_prod, List.Nodup.length_le_enatCard, Order.length_le_coheight_head, Matrix.eRank_submatrix_le, SimpleGraph.chromaticNumber_mono_of_hom, ENat.ceil_le_floor_add_one, Matroid.eRk_submod, IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton, Monoid.minOrder_le_orderOf, Dynamics.one_le_netMaxcard_iff, Metric.coveringNumber_anti, Cardinal.natCast_le_toENat_iff, Polynomial.trailingDegree_one_le, multiplicity_le_emultiplicity, Set.encard_le_one_iff_subsingleton, AddMonoid.minOrder_le_natCard, PowerSeries.le_weightedOrder_subst, Order.height_eq_coe_iff_minimal_le_height, ENat.lt_coe_add_one_iff, ContDiffMapSupportedIn.structureMapLM_apply, ENat.card_le_one, Polynomial.le_trailingDegree_X, Dynamics.le_coverMincard_image, Matroid.spanning_iff_eRk_le, MvPowerSeries.le_order_pow_of_constantCoeff_eq_zero, Order.coheight_le_iff, natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero, Polynomial.emultiplicity_le_one_of_separable, PowerSeries.le_order_subst_left, ENat.one_le_iff_ne_zero, ENat.floor_le, Set.encard_le_encard_diff_add_encard, SimpleGraph.edist_le_one_iff_adj_or_eq, SimpleGraph.IsAcyclic.chromaticNumber_le_two, Metric.coveringNumber_le_one_of_ediam_le, MvPowerSeries.le_order_map
|
instLTENat 📖 | CompOp | 148 mathmath: Matroid.eRk_lt_top_iff, ENat.add_lt_top, Cardinal.natCast_lt_toENat_iff, ENat.add_lt_add, ENat.toENNReal_lt_top, ENat.floor_pos, ENat.top_pos, ENat.lt_add_one_iff', Matroid.eRk_lt_encard_iff_dep, Cardinal.ofENat_lt_ofNat, ENat.card_lt_top, SimpleGraph.chromaticNumber_pos, ENat.card_pos, Ideal.height_lt_top, ENat.one_lt_card_iff_nontrivial, Dynamics.coverMincard_finite_of_isCompact_invariant, SimpleGraph.ediam_eq_top, lt_emultiplicity_of_lt_multiplicity, Topology.RelCWComplex.coe_skeletonLT, Order.height_pos, Topology.CWComplex.iUnion_openCell_eq_skeletonLT, emultiplicity_lt_iff_not_dvd, emultiplicity_pos_of_dvd, Ideal.primeHeight_lt_top, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, Ideal.height_strict_mono_of_is_prime, PowerSeries.order_finite_iff_ne_zero, Matroid.eRk_lt_encard_iff_dep_of_finite, Topology.RelCWComplex.mem_skeletonLT_iff, Topology.RelCWComplex.iUnion_openCell_eq_skeleton, Cardinal.ofENat_lt_aleph0, ENat.lt_top_of_sum_ne_top, Submodule.length_lt, Order.coheight_eq_coe_add_one_iff, Topology.CWComplex.mem_skeletonLT_iff, Module.length_pos_iff, Mathlib.Tactic.ENatToNat.not_lt_top, ENat.lt_lift_iff, Cardinal.toENat_lt_natCast_iff, Set.Finite.encard_lt_top, ENat.card_lt_top_of_finite, ENat.add_one_le_iff, ENat.iInf_coe_lt_top, ENat.ceil_lt_top, ENat.sum_lt_top, Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt, Cardinal.natCast_lt_toENat, ENat.eq_top_iff_forall_gt, Dynamics.coverMincard_finite_of_isCompact_uniformContinuous, Order.coheight_pos_of_lt_top, Ideal.primeHeight_strict_mono, Order.height_pos_of_bot_lt, ENat.ceil_lt, Set.encard_lt_top_iff, SimpleGraph.edist_pos_of_ne, Cardinal.toENat_lt_natCast, Set.Finite.encard_lt_encard, ENat.ceil_pos, Matroid.IsRkFinite.eRk_lt_top, SimpleGraph.vertexCoverNum_lt_card, ENat.lt_ceil, Matroid.eRank_lt_top_iff, ENat.prod_lt_top, ENat.natCast_lt_succ, Order.height_strictMono, Nat.emultiplicity_two_factorial_lt, ENat.floor_lt_ceil, Ideal.height_le_iff, ENat.floor_lt_top, Order.height_eq_coe_add_one_iff, Order.height_le_coe_iff, Order.height_eq_coe_iff, ENat.toENNReal_lt, Cardinal.ofNat_lt_ofENat, Set.Nonempty.encard_pos, Metric.coveringNumber_pos_iff, MeasureTheory.stoppedValue_sub_eq_sum', Cardinal.toENat_lt_ofNat, dvd_iff_emultiplicity_pos, ENat.lift_lt_iff, ENat.add_lt_add_iff_left, Ideal.height_le_iff_covBy, SimpleGraph.eccent_pos_iff, Module.length_pos, Set.encard_lt_one, ENat.pow_lt_top_iff, ENat.epow_def, Polynomial.trailingDegree_lt_wf, Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT, FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt, ENat.lt_add_one_iff, Cardinal.ofENat_lt_ofENat, Cardinal.toENat_lt_one, ENat.coe_lt_coe, emultiplicity_lt_top, Matroid.eRk_lt_encard_of_dep_of_finite, Order.coe_lt_coheight_iff, ENat.add_one_pos, Order.coheight_le_coe_iff, Cardinal.one_lt_ofENat, Topology.CWComplex.iUnion_openCell_eq_skeleton, ENat.add_lt_add_of_le_of_lt, Dynamics.netMaxcard_finite_iff, Cardinal.ofENat_lt_nat, ENat.floor_lt, Cardinal.ofENat_pos, Set.one_lt_encard_iff, Set.encard_pos, Set.Finite.ecard_lt_ecard, Set.encard_lt_encard_iff_encard_diff_lt_encard_diff, ENat.sum_lt_sum_of_nonempty, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map, Ideal.finiteHeight_iff_lt, Order.coheight_eq_coe_iff, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, ENat.one_lt_top, ENat.lt_floor, Matroid.Dep.eRk_lt_encard, Dynamics.coverMincard_finite_iff, Set.one_lt_encard_iff_nontrivial, emultiplicity_pos_iff, Metric.externalCoveringNumber_pos_iff, ENat.exists_nat_gt, Topology.RelCWComplex.skeletonLT_I, ENat.card_pos_iff_nonempty, Order.coheight_pos, Metric.packingNumber_pos_iff, ENat.add_lt_add_of_lt_of_le, ENat.tendsto_nhds_top_iff_natCast_lt, ENat.lift_add, SimpleGraph.two_lt_edist_iff, Cardinal.one_lt_toENat, ENat.one_lt_card, Order.coe_lt_height_iff, Submodule.height_lt_top, Cardinal.ofNat_lt_toENat, Stream'.Seq.lt_length'_iff, ENat.add_lt_add_iff_right, Mathlib.Meta.Positivity.natCeil_pos, ENat.lt_coe_add_one_iff, Cardinal.toENat_lt_top, Order.one_lt_height_iff, ENat.iSup_coe_lt_top, ENat.lt_one_iff_eq_zero, ENat.not_lt_zero, ENat.coe_lt_top, Cardinal.nat_lt_ofENat, Order.coheight_strictAnti
|
instLinearOrderENat 📖 | CompOp | 27 mathmath: ContDiffMapSupportedIn.iteratedFDerivLM_apply, ContDiffMapSupportedIn.structureMapCLM_apply, emultiplicity_add_eq_min, ContDiffMapSupportedIn.monoLM_apply, Order.krullDim_le_of_krullDim_preimage_le, MvPowerSeries.min_weightedOrder_le_add, ContDiffMapSupportedIn.monoCLM_apply, ENat.mul_top', ENat.toENNReal_min, IsDiscreteValuationRing.addVal_add, TestFunction.lineDerivCLM_apply, PowerSeries.min_order_le_order_add, ENat.epow_def, Polynomial.ringKrullDim_le, MvPowerSeries.weightedOrder_add_of_weightedOrder_ne, ContDiffMapSupportedIn.fderivLM_apply, ENat.toENNReal_max, TestFunction.monoCLM_apply, MvPowerSeries.order_add_of_order_ne, ContDiffMapSupportedIn.fderivCLM_apply, TestFunction.fderivCLM_apply, min_le_emultiplicity_add, PowerSeries.order_add_of_order_ne, MvPowerSeries.min_order_le_add, ContDiffMapSupportedIn.structureMapLM_apply, Order.krullDim_le_of_krullDim_preimage_le', ENat.top_mul'
|
instLinearOrderedAddCommMonoidWithTopENat 📖 | CompOp | 34 mathmath: IsDiscreteValuationRing.addVal_zero, Finset.set_encard_biUnion_le, Finset.emultiplicity_prod, ENat.iInf_sum, ENat.sum_iSup, multiplicity_addValuation_apply, Set.encard_iUnion_of_finite, ENat.sum_lt_top, 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, ENat.sum_eq_top, IsDiscreteValuationRing.addVal_eq_zero_of_unit, ENat.sum_lt_sum_of_nonempty, Set.Finite.encard_biUnion, IsDiscreteValuationRing.addVal_def, MvPowerSeries.order_prod, IsDiscreteValuationRing.addVal_one, ENat.sum_iSup_of_monotone, IsDiscreteValuationRing.addVal_le_iff_dvd, Set.encard_iUnion_le_of_fintype, Set.Finite.encard_biUnion_le, PowerSeries.le_order_prod, ENat.toNat_sum, 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 | — |
instPreorderENat 📖 | CompOp | 238 mathmath: Dynamics.netMaxcard_monotone_subset, Cardinal.natCast_lt_toENat_iff, Order.LTSeries.length_le_krullDim, Order.krullDim_le_of_strictComono_and_surj, ringKrullDim_succ_le_ringKrullDim_polynomial, Set.toENat_cardinalMk_subtype, Cardinal.toENat_eq_natCast_iff, Order.krullDim_lt_coe_iff, Set.Finite.ecard_strictMonoOn, CategoryTheory.Retract.injectiveDimension_le, Module.End.isNilpotent_restrict_genEigenspace_nat, ModuleCat.injectiveDimension_eq_iSup_localizedModule_prime, CategoryTheory.injectiveDimension_le_iff, Cardinal.toENat_ofENat, Order.krullDim_nonneg_iff, Matroid.eRk_mono, Ring.krullDimLE_iff, ENat.gc_toENNReal_floor, Module.length_of_free, ENat.natCast_le_of_coe_top_le_withTop, Module.End.independent_genEigenspace, ENat.toENNReal_strictMono, Module.End.genEigenspace_mem_invtSubmodule, Order.krullDim_pos_iff, Order.krullDim_le_one_iff, Module.End.genEigenspace_directed, ENat.monotone_map_iff, Submodule.spanRank_toENat_eq_iInf_encard, Module.End.maxGenEigenspace_eq, Cardinal.toENat_eq_zero, Order.le_krullDim_iff, Cardinal.toENat_eq_ofNat, Module.End.maxGenEigenspace_eq_genEigenspace_finrank, Module.End.mapsTo_genEigenspace_of_comm, Cardinal.ofENat_mono, ENat.add_one_natCast_le_withTop_of_lt, le_minSmoothness, ringKrullDim_succ_le_ringKrullDim_powerseries, Dynamics.coverMincard_monotone_time, Order.coheight_le_krullDim, ENat.map_natCast_strictMono, Order.krullDim_nonpos_iff_forall_isMax, ringKrullDim_nonneg_of_nontrivial, ContinuousLinearMap.isClosed_genEigenspace, Order.krullDim_nonpos_iff_forall_isMin, Set.ecard_strictMono, Cardinal.toENat_lt_natCast_iff, Module.supportDim_le_of_injective, Cardinal.ofNat_eq_toENat, Submodule.inf_genEigenspace, Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex, Set.encard_strictMono, Submodule.height_strictMono, Order.krullDim_le_of_krullDim_preimage_le, Cardinal.toENat_lift, ENat.instOrderTopology, Order.height_le_krullDim, Cardinal.toENat_le_ofNat, CategoryTheory.injectiveDimension_ge_iff, Cardinal.natCast_lt_toENat, Order.bot_lt_krullDim, topologicalKrullDim_subspace_le, LinearMap.finrank_genEigenspace_le, topologicalKrullDim_zero_of_discreteTopology, ringKrullDim_quotient_le, Module.End.iSup_genEigenspace_eq, Module.End.genEigenspace_inf_le_add, Module.End.eigenspace_le_genEigenspace, ENat.succ_top, ringKrullDim_succ_le_of_surjective, Ideal.primeHeight_le_ringKrullDim, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, CategoryTheory.projectiveDimension_lt_iff, ENat.epow_right_mono, Cardinal.toENat_lt_natCast, ENat.WithBot.add_le_add_natCast_left_iff, ringKrullDim_le_iff_height_le, Dynamics.coverMincard_antitone, Dynamics.netMaxcard_antitone, Order.krullDim_nonpos_of_subsingleton, IsInducing.topologicalKrullDim_le, ringKrullDim_le_ringKrullDim_quotient_add_card, Cardinal.toENat_ofNat, Ideal.height_le_ringKrullDim_quotient_add_one, ENat.gc_ceil_toENNReal, Module.End.disjoint_genEigenspace, ENat.one_le_iff_ne_zero_withTop, Submodule.inf_iSup_genEigenspace, ringKrullDim_le_spanFinrank_maximalIdeal, IsClosedEmbedding.topologicalKrullDim_le, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, Order.krullDim_enat, Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, Module.End.mem_genEigenspace_top, Module.End.injOn_genEigenspace, Module.End.genEigenspace_one, ENat.LEInfty.out, Order.krullDim_le_one_iff_of_boundedOrder, Cardinal.toENatAux_gc, Cardinal.toNat_toENat, Cardinal.natCast_le_toENat, ENat.toENNReal_mono, ENat.floor_mono, Ideal.height_le_ringKrullDim_quotient_add_encard, tangentBundleCore.isContMDiff, ENat.epow_left_mono, Order.krullDim_eq_iSup_coheight, TangentBundle.contMDiffVectorBundle, toENat_rank_span_set, Set.encard_mono, Cardinal.toENat_lt_ofNat, Cardinal.toENat_le_natCast, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, Dynamics.netMaxcard_monotone_time, Cardinal.toENat_strictMonoOn, Order.krullDim_eq_iSup_height, ENat.WithBot.add_le_add_one_left_iff, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, Submodule.spanRank_toENat_eq_iInf_finset_card, Order.one_le_krullDim_iff, Order.krullDim_le_of_strictMono, Cardinal.continuum_toENat, ringKrullDim_le_iff_isMaximal_height_le, ringKrullDim_le_ringKrullDim_add_card, CategoryTheory.projectiveDimension_le_iff, Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, ModuleCat.projectiveDimension_le_projectiveDimension_of_isLocalizedModule, Module.supportDim_le_ringKrullDim, Module.supportDim_le_supportDim_quotSMulTop_succ, CategoryTheory.projectiveDimension_ge_iff, ENat.WithBot.add_one_le_iff, Module.End.genEigenspace_zero_nat, Submodule.eq_iSup_inf_genEigenspace, Module.End.genEigenspace_top, ringKrullDim_lt_top, CategoryTheory.injectiveDimension_lt_iff, Cardinal.ofENat_strictMono, Cardinal.toENat_lt_one, ENat.ceil_mono, Polynomial.ringKrullDim_le, Cardinal.toENat_le_iff_of_le_aleph0, Cardinal.toENat_eq_top, Cardinal.ofNat_le_toENat, ENat.WithBot.add_le_add_natCast_right_iff, Topology.RelCWComplex.skeleton_monotone, ModuleCat.injectiveDimension_le_injectiveDimension_of_isLocalizedModule, Order.krullDim_le_one_iff_forall_isMax, Module.End.generalized_eigenvec_disjoint_range_ker, Order.krullDim_pos_iff_of_orderTop, ModuleCat.projectiveDimension_eq_iSup_localizedModule_maximal, Module.End.isNilpotent_restrict_sub_algebraMap, Cardinal.toENat_le_natCast_iff, Set.toENat_cardinalMk, Order.coheight_coe_enat, ENat.mul_left_strictMono, Module.End.mem_genEigenspace_one, Cardinal.enat_gc, Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace, Cardinal.toENat_le_nat, Order.krullDim_pos_iff_of_orderBot, Cardinal.toENat_eq_natCast, Module.End.genEigenspace_div, Module.End.genEigenspace_eq_genEigenspace_finrank_of_le, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, SimpleGraph.egirth_anti, Module.End.genEigenspace_nat, height_le_ringKrullDim_quotient_add_spanFinrank, ENat.succ_coe, Cardinal.toENat_comp_ofENat, ENat.strictMono_map_iff, Module.End.genEigenspace_le_maximal, Cardinal.toENat_le_iff_of_lt_aleph0, Module.End.mem_genEigenspace_nat, Cardinal.ofENat_toENat_le, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, ENat.WithBot.lt_add_one_iff, Cardinal.toENat_le_one, Cardinal.toENat_injOn, LinearIndepOn.encard_le_toENat_rank, Cardinal.toENat_eq_nat, Order.KrullDimLE.krullDim_le, Module.End.isNilpotent_restrict_genEigenspace_top, ringKrullDim_le_ringKrullDim_add_spanFinrank, ENat.succ_def, Cardinal.ofENat_toENat_eq_self, Order.coheight_anti, Cardinal.ofENat_toENat, Order.height_mono, Cardinal.aleph_toENat, Cardinal.one_le_toENat, Order.krullDim_nonneg, exist_minSmoothness_le_ne_infty, Module.End.genEigenspace_restrict_eq_top, Cardinal.toENat_eq_iff_of_le_aleph0, Order.krullDim_le_one_iff_forall_isMin, Module.End.hasGenEigenvector_iff, Module.End.mem_genEigenspace_zero, Ideal.height_le_spanRank_toENat, Cardinal.natCast_eq_toENat_iff, CategoryTheory.Retract.projectiveDimension_le, Module.End.genEigenspace_le_genEigenspace_finrank, Module.End.mem_genEigenspace, Cardinal.toENat_nat, Topology.RelCWComplex.skeletonLT_monotone, Cardinal.one_lt_toENat, Ideal.height_le_ringKrullDim_of_ne_top, Module.End.genEigenspace_zero, Matroid.toENat_cRank_eq, Order.height_enat, ENat.mul_right_strictMono, ModuleCat.projectiveDimension_eq_iSup_localizedModule_prime, ringKrullDim_le_of_surjective, minSmoothness_monotone, Module.End.genEigenspace_le_smul, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, ModuleCat.injectiveDimension_eq_iSup_localizedModule_maximal, ENat.WithBot.add_le_add_one_right_iff, Module.supportDim_le_of_surjective, Module.End.genEigenspace_restrict, ENat.natCast_lt_of_coe_top_le_withTop, Cardinal.ofNat_lt_toENat, Cardinal.natCast_le_toENat_iff, Set.Finite.encard_strictMonoOn, Order.bot_lt_krullDim_iff, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, Module.length_eq_rank, Order.krullDim_le_of_krullDim_preimage_le', Cardinal.toENat_lt_top, Cardinal.toENat_congr, ENat.range_natCast, Matroid.toENat_cRk_eq, ringKrullDim_le_ringKrullDim_quotient_add_encard, Order.krullDimLE_iff, Cardinal.toENat_eq_one, Cardinal.natCast_eq_toENat, Dynamics.coverMincard_monotone_subset
|
instSubENat 📖 | CompOp | 38 mathmath: ENat.sub_iInf, 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 | 3 mathmath: ENat.succ_top, ENat.succ_coe, ENat.succ_def
|
instWellFoundedLTENat 📖 | CompOp | — |
instZeroLEOneClassENat 📖 | CompOp | — |