instNatCast 📖 | CompOp | 354 mathmath: Cardinal.natCast_lt_toENat_iff, Topology.RelCWComplex.skeletonLT_union_iUnion_closedCell_eq_skeletonLT_succ, Module.length_compositionSeries, Nat.Prime.emultiplicity_choose_prime_pow_add_emultiplicity, Ideal.height_le_spanFinrank, MvPowerSeries.weightedOrder_monomial, Cardinal.toENat_eq_natCast_iff, Cardinal.ofENat_lt_ofNat, coe_one, SimpleGraph.le_chromaticNumber_iff_colorable, SimpleGraph.le_chromaticNumber_iff_coloring, AddCircle.card_torsion_le_of_isSMulRegular, Cardinal.ofENat_le_ofNat, Set.ncard_le_encard, untopD_coe_enat, PartENat.toWithTop_natCast, Order.length_le_coheight, Ideal.exists_finset_card_eq_height_of_isNoetherianRing, SimpleGraph.Walk.edist_le, Set.encard_pair, canLift, Mathlib.Tactic.ENatToNat.coe_sub, iInf_toNat, Order.height_nat, Module.End.genEigenspace_directed, lt_emultiplicity_of_lt_multiplicity, ceil_add_natCast, Topology.RelCWComplex.coe_skeletonLT, Module.End.maxGenEigenspace_eq, AddMonoid.minOrder_le_addOrderOf, Nat.count_le_setENCard, SimpleGraph.two_le_chromaticNumber_of_adj, Topology.RelCWComplex.cellFrontier_subset_skeletonLT, SimpleGraph.card_le_chromaticNumber_iff_forall_surjective, Subgroup.IsComplement.encard_left, SimpleGraph.exists_egirth_eq_length, Topology.CWComplex.iUnion_openCell_eq_skeletonLT, emultiplicity_lt_iff_not_dvd, SimpleGraph.three_le_egirth, Dynamics.IsDynNetIn.card_le_netMaxcard, Cardinal.ofENat_eq_ofNat, SimpleGraph.chromaticNumber_cycleGraph_of_even, Stream'.Seq.length'_of_terminates, Module.End.maxGenEigenspace_eq_genEigenspace_finrank, Nat.Prime.emultiplicity_factorial, floor_add_natCast, forall_natCast_le_iff_le, ZMod.minOrder_of_prime, Nat.cast_analyticOrderNatAt, SimpleGraph.chromaticNumber_top, SimpleGraph.Colorable.chromaticNumber_eq_sInf, epow_natCast, Ideal.exists_ltSeries_length_eq_height, MvPowerSeries.weightedOrder_monomial_of_ne_zero, ZMod.minOrder, FiniteMultiplicity.emultiplicity_eq_multiplicity, Topology.RelCWComplex.iUnion_openCell_eq_skeleton, Stream'.Seq.length'_le_iff, Cardinal.toENatAux_eq_nat, MvPowerSeries.nat_le_order, Nat.Prime.emultiplicity_factorial_mul, ne_top_iff_exists, Order.coheight_eq_coe_add_one_iff, Subgroup.IsComplement.encard_right, measurable_iff, Monoid.minOrder_le_natCard, lt_lift_iff, Mathlib.Tactic.ENatToNat.coe_mul, AddMonoid.le_minOrder, Cardinal.toENat_lt_natCast_iff, Polynomial.le_trailingDegree_monomial, Cardinal.toENatAux_nat, MvPowerSeries.nat_le_weightedOrder, Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex, Cardinal.nat_eq_ofENat, emultiplicity_pow_prime_pow_sub_pow_prime_pow, Module.End.map_genEigenrange_le, Set.coe_fintypeCard, Polynomial.trailingDegree_C_mul_X_pow, iInf_coe_lt_top, FiniteMultiplicity.emultiplicity_eq_iff_multiplicity_eq, analyticOrderAt_centeredMonomial, le_emultiplicity_of_le_multiplicity, SimpleGraph.chromaticNumber_eq_iInf, Stream'.Seq.drop_length', Topology.RelCWComplex.cellFrontier_subset_skeleton, eq_top_iff_forall_gt, LinearMap.finrank_genEigenspace_le, Ideal.height_le_card_of_mem_minimalPrimes_span, SimpleGraph.chromaticNumber_le_card, Module.End.iSup_genEigenspace_eq, SimpleGraph.chromaticNumber_eq_two_iff, Set.encard_eq_three, Nat.Prime.emultiplicity_choose', coe_sSup, coe_toNat_le_self, Module.End.eigenspace_le_genEigenspace, PartENat.withTopEquiv_ofNat, AddSubgroup.IsComplement.encard_right, AddSubgroup.IsComplement.encard_left, PowerSeries.order_monomial, IsDiscreteValuationRing.addVal_def', Order.krullDim_eq_iSup_length, Dynamics.IsDynCoverOf.coverMincard_le_card, Irreducible.addVal_pow, Order.coheight_eq_coe_iff_maximal_le_coheight, ContDiffMapSupportedIn.iteratedFDerivWithOrderLM_apply, SimpleGraph.chromaticNumber_le_iff_colorable, SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable, Topology.RelCWComplex.openCell_subset_skeletonLT, toNat_eq_iff, Topology.RelCWComplex.closedCell_subset_skeletonLT, Set.Nat.encard_range, coe_toNat, emultiplicity_pow_self, MvPowerSeries.ne_zero_iff_weightedOrder_finite, SimpleGraph.chromaticNumber_eq_card_iff, natCast_le_analyticOrderAt, Order.coheight_eq_iSup_head_eq, coe_mul, Nat.Prime.emultiplicity_choose, Int.two_pow_two_pow_add_two_pow_two_pow, coe_iSup, Submodule.spanFinrank_span_le_encard, ContDiffMapSupportedIn.structureMapLM_apply_withOrder, natCast_lt_succ, iInf_eq_top_of_isEmpty, Nat.emultiplicity_two_factorial_lt, le_emultiplicity_of_pow_dvd, iInf_coe_eq_top, Ideal.height_le_iff, SimpleGraph.chromaticNumber_le_two_iff_isBipartite, SimpleGraph.CompleteBipartiteGraph.chromaticNumber, SimpleGraph.two_le_chromaticNumber_iff_ne_bot, ceil_natCast_add, Topology.RelCWComplex.skeleton_union_iUnion_closedCell_eq_skeleton_succ, MeasureTheory.stoppedProcess_eq, Order.height_eq_coe_add_one_iff, floor_sub_natCast, floor_coe, Polynomial.trailingDegree_le_of_ne_zero, PowerSeries.coe_toNat_order, FiniteMultiplicity.emultiplicity_le_of_multiplicity_le, AnalyticAt.analyticOrderAt_eq_natCast, SimpleGraph.le_chromaticNumber_iff_forall_surjective, Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le, Order.height_le_coe_iff, Topology.RelCWComplex.iUnion_skeletonLT_eq_complex, Order.height_eq_coe_iff, Polynomial.le_trailingDegree_C_mul_X_pow, Cardinal.ofNat_lt_ofENat, SimpleGraph.Colorable.chromaticNumber_le, ceil_sub_natCast, coe_iInf, lift_le_iff, PowerSeries.le_order_pow_of_constantCoeff_eq_zero, toNatHom_apply, Order.length_le_height, MvPowerSeries.order_le, coe_toNat_eq_self, Nat.Prime.emultiplicity_choose_prime_pow, Order.coheight_le_of_krullDim_preimage_le, AddCircle.card_torsion_le_of_isSMulRegular_int, iSup_natCast, Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton, coe_inj, pow_dvd_iff_le_emultiplicity, SimpleGraph.cliqueNum_le_chromaticNumber, Polynomial.natTrailingDegree_le_trailingDegree, PartENat.toWithTop_natCast', Set.encard_eq_coe_toFinset_card, SimpleGraph.ediam_le_two_mul_radius, Topology.RelCWComplex.iUnion_cellFrontier_subset_skeletonLT, Cardinal.ofENat_eq_nat, SimpleGraph.edist_eq_sInf, top_sub_coe, PartENat.withTopEquiv_natCast, lift_lt_iff, Order.height_le_of_krullDim_preimage_le, Ideal.height_le_iff_covBy, SimpleGraph.chromaticNumber_cycleGraph_of_odd, coe_sub, AddMonoid.le_minOrder_iff_forall_addSubgroup, Module.End.genEigenspace_eq_iSup_genEigenspace_nat, SimpleGraph.Connected.exists_walk_length_eq_edist, Cardinal.ofNat_le_ofENat, coe_lift, addLECancellable_coe, Submodule.spanRank_toENat_eq_iInf_finset_card, Set.encard_le_coe_iff_finite_ncard_le, coe_sInf, Mathlib.Tactic.ENatToNat.coe_zero, Order.coheight_le_iff', mem_nhds_natCast_iff, recTopCoe_coe, MvPowerSeries.weightedOrder_eq_nat, Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT, Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex, le_coe_iff, ContDiffMapSupportedIn.structureMapCLM_apply_withOrder, Monoid.le_minOrder_iff_forall_subgroup, Mathlib.Tactic.ENatToNat.coe_ofNat, nhds_natCast, Module.End.genEigenspace_zero_nat, FiniteMultiplicity.emultiplicity_lt_of_multiplicity_lt, SimpleGraph.le_chromaticNumber_of_pairwise_adj, Module.End.genEigenspace_top, Cardinal.ofENat_nat, Topology.RelCWComplex.openCell_subset_skeleton, PartENat.toWithTop_some, Module.End.genEigenrange_nat, PartENat.ofENat_coe, card_eq_coe_fintype_card, coe_lt_coe, PowerSeries.order_le, iSup_coe_eq_top, coe_le_coe, Order.coe_lt_coheight_iff, MvPowerSeries.weightedOrder_le, Order.coheight_le_coe_iff, SimpleGraph.completeMultipartiteGraph.chromaticNumber, Topology.CWComplex.iUnion_openCell_eq_skeleton, UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors, Set.Finite.exists_encard_eq_coe, Dynamics.netMaxcard_finite_iff, Set.encard_eq_four, Set.Finite.encard_eq_coe, Cardinal.ofENat_lt_nat, MeasureTheory.stoppedProcess_eq', Module.End.generalized_eigenvec_disjoint_range_ker, Nat.Prime.emultiplicity_pow, Set.encard_coe_eq_coe_finsetCard, Nat.Prime.emultiplicity_factorial_le_div_pred, UniqueFactorizationMonoid.le_emultiplicity_iff_replicate_le_normalizedFactors, Cardinal.toENat_le_natCast_iff, cauchy_davenport_minOrder_add, SimpleGraph.chromaticNumber_eq_biInf, Order.coheight_coe_enat, Cardinal.toENatAux_le_nat, map_coe, Cardinal.toENat_le_nat, SimpleGraph.egirth_le_length, Set.encard_le_coe_iff, isEmbedding_natCast, Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq, MvPowerSeries.ne_zero_iff_order_finite, Module.End.genEigenspace_eq_genEigenspace_finrank_of_le, Set.encard_eq_two, floor_natCast_add, MvPowerSeries.order_monomial, toENNReal_coe, SimpleGraph.IsClique.card_le_chromaticNumber, PartENat.toWithTop_ofNat, lift_coe, Module.End.genEigenspace_nat, Order.coheight_eq_coe_iff, SimpleGraph.exists_walk_of_edist_ne_top, Module.End.genEigenspace_le_maximal, toNat_coe, Module.End.mem_genEigenspace_nat, emultiplicity_eq_coe, Set.Finite.encard_eq_coe_toFinset_card, Module.length_eq_finrank, Topology.RelCWComplex.iUnion_skeleton_eq_complex, IsDiscreteValuationRing.addVal_def, Int.two_pow_two_pow_sub_pow_two_pow, Order.height_le_iff, emultiplicity_pow, PartENat.withTopEquiv_symm_coe, Dynamics.coverMincard_finite_iff, Cardinal.toENat_eq_nat, emultiplicity_eq_iff_multiplicity_eq_of_ne_one, emultiplicity_eq_of_dvd_of_not_dvd, Cardinal.nat_le_ofENat, SimpleGraph.Reachable.coe_dist_eq_edist, exists_nat_gt, toNat_eq_iff_eq_coe, Topology.RelCWComplex.skeletonLT_I, Order.height_le_iff', MvPowerSeries.order_eq_nat, Ideal.height_le_height_add_spanFinrank_of_le, Order.index_le_height, Order.coheight_eq, forall_ne_top, SimpleGraph.le_egirth, Nat.Prime.emultiplicity_pow_self, ceil_coe, SimpleGraph.chromaticNumber_eq_iff_forall_surjective, Module.End.hasGenEigenvector_iff, tendsto_nhds_top_iff_natCast_lt, SimpleGraph.edist_le, le_lift_iff, Polynomial.trailingDegree_eq_natTrailingDegree, Monoid.le_minOrder, Submodule.FG.exists_span_set_encard_eq_spanFinrank, SimpleGraph.Reachable.exists_walk_length_eq_edist, Order.rev_index_le_coheight, Mathlib.Tactic.ENatToNat.coe_add, Cardinal.natCast_eq_toENat_iff, cauchy_davenport_minOrder_mul, eq_top_iff_forall_ge, Cardinal.ofENat_le_nat, coe_zero, Module.length_of_free_of_finite, SimpleGraph.chromaticNumber_pathGraph, Module.End.genEigenspace_le_genEigenspace_finrank, Module.End.mem_genEigenspace, le_emultiplicity_iff_replicate_subperm_primeFactorsList, Ideal.height_le_card_of_mem_minimalPrimes_span_finset, Cardinal.toENat_nat, PowerSeries.nat_le_order, Set.Finite.cast_ncard_eq, emultiplicity_pow_self_of_prime, Polynomial.le_trailingDegree_X_pow, PowerSeries.order_X_pow, Order.height_eq_iSup_last_eq, Nat.emultiplicity_eq_card_pow_dvd, Order.length_le_height_last, SimpleGraph.Walk.three_le_chromaticNumber_of_odd_loop, Order.coe_lt_height_iff, Polynomial.trailingDegree_monomial, coe_add, MvPowerSeries.order_monomial_of_ne_zero, Mathlib.Tactic.ENatToNat.coe_one, Cardinal.ofNat_eq_ofENat, Order.length_le_coheight_head, Topology.RelCWComplex.closedCell_subset_skeleton, Monoid.minOrder_le_orderOf, Cardinal.natCast_le_toENat_iff, Stream'.Seq.lt_length'_iff, padicValNat.maxPowDiv_eq_emultiplicity, multiplicity_le_emultiplicity, AddMonoid.minOrder_le_natCard, Order.height_eq_coe_iff_minimal_le_height, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue, lt_coe_add_one_iff, SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective, MvPowerSeries.le_order_pow_of_constantCoeff_eq_zero, Polynomial.trailingDegree_X_pow, Polynomial.IsDistinguishedAt.coe_natDegree_eq_order_map, Order.coheight_le_iff, natCast_le_analyticOrderAt_iff_iteratedDeriv_eq_zero, iSup_coe_lt_top, range_natCast, isOpenEmbedding_natCast, PowerSeries.order_monomial_of_ne_zero, padicValNat_eq_emultiplicity, card_eq_coe_natCard, exists_ne_top, Polynomial.trailingDegree_eq_iff_natTrailingDegree_eq_of_pos, coe_lt_top, Cardinal.nat_lt_ofENat, PowerSeries.order_eq_nat, Set.chainHeight_eq_top_iff
|