Cardinal 📖 | CompOp | 1207 mathmath: Cardinal.lt_ord_succ_card, Cardinal.mk_le_of_module, Cardinal.aleph_le_beth, Cardinal.toNat_ofENat, Cardinal.natCast_lt_toENat_iff, Cardinal.toNat_surjective, Cardinal.mk_eq_zero, Module.rank_lt_aleph0_iff, Ordinal.lift_card_iSup_le_sum_card, Cardinal.mk_le_of_surjective, Cardinal.toNat_ofNat, Cardinal.continuum_mul_ofNat, Cardinal.mk_sUnion_le, Cardinal.ofENat_le_lift, Submodule.fg_iff_spanRank_eq_spanFinrank, Module.rank_def, Cardinal.add_le_aleph0, Algebra.lift_cardinalMk_adjoin_le, Cardinal.lift_le_ofENat, SymmetricAlgebra.rank_eq, natCast_le_rank_iff_finset, Ordinal.cof_iSup_le_lift, Subalgebra.adjoin_rank_le, Ideal.height_le_spanRank, Cardinal.powerlt_max, Cardinal.mk_insert_le, Cardinal.le_mk_iff_exists_subset, Cardinal.mk_add_one_eq, Cardinal.mk_emptyCollection_iff, Cardinal.le_beth_ord, HahnSeries.mem_cardSuppLTSubfield, Ordinal.sInf_compl_lt_lift_ord_succ, Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic, Ordinal.cof_blsub_le, Set.toENat_cardinalMk_subtype, Cardinal.toENat_eq_natCast_iff, Cardinal.ofENat_lt_lift, linearIndependent_le_span, rank_le_card_isVisible, Cardinal.lift_mk_le, lift_rank_mul_lift_rank, HahnSeries.cardSupp_single_of_ne, Algebraic.cardinalMk_lift_le_mul, trdeg_eq_zero_of_not_injective, Cardinal.mk_list_eq_max_mk_aleph0, Ordinal.card_le_ofNat, Cardinal.ofENat_lt_ofNat, IsNoetherian.iff_rank_lt_aleph0, Ideal.height_le_iff_exists_minimalPrimes, Cardinal.mk_list_le_max, LinearIndependent.cardinal_lift_le_rank, Matrix.lift_cRank_submatrix_le, lift_rank_map_le, Cardinal.aleph_succ, linearIndependent_le_span_finset, Matroid.Indep.cardinalMk_le_cRk_of_subset, LinearMap.rank_le_domain, Ordinal.isInitialIso_apply, Ideal.rank_prime_pow_ramificationIdx, Cardinal.preBeth_eq_zero, Cardinal.ofENat_ofNat, Cardinal.mk_preimage_of_subset_range_lift, Cardinal.two_le_iff_one_lt, Cardinal.mk_multiset_of_nonempty, Quaternion.rank_eq_four, Cardinal.aleph_pos, Cardinal.aleph0_add_nat, Cardinal.mk_embedding_le_arrow, Cardinal.toNat_eq_iff, Cardinal.aleph0_le_continuum, Cardinal.le_sum, Cardinal.aleph0_mul_ofNat, rank_le_one, HahnSeries.coe_cardSuppLTAddSubmonoid, Cardinal.toNat_congr, Ordinal.cof_zero, Cardinal.ofENat_le_ofNat, Cardinal.toENat_ofENat, Cardinal.power_mul, Algebra.IsAlgebraic.trdeg_le_cardinalMk, Cardinal.mk_subtype_le_of_subset, Subfield.relrank_dvd_of_le_left, Cardinal.iSup_of_empty, Computability.Encoding.card_le_aleph0, HahnSeries.cardSupp_smul_le, Submodule.spanRank_map_le, Cardinal.mk_subtype_mono, Cardinal.ord.orderEmbedding_coe, rank_finsupp, Cardinal.ofNat_le_lift_iff, linearIndependent_le_span', Cardinal.one_eq_ofENat, Module.length_of_free, Cardinal.lift_le_aleph0, Field.insepDegree_le_rank, Cardinal.mk_equiv_le_embedding, Cardinal.nat_add_continuum, Field.insepDegree_mul_insepDegree_of_isAlgebraic, AddOreLocalization.cardinalMk_le, Cardinal.isPrimePow_iff, Cardinal.range_ofENat, LinearMap.lift_rank_le_of_surjective, Cardinal.lift_eq_aleph_one, Cardinal.sum_zero_pow, aleph0_le_rank_of_isEmpty_oreSet, Ordinal.card_le_aleph, Filter.cardinalInterFilter_sup, Cardinal.sum_pow_le_max_aleph0, Matrix.cRank_subsingleton, OrdinalApprox.gfpApprox_ord_mem_fixedPoint, exists_spanRank_le_and_le_height_of_le_height, Cardinal.nat_mul_aleph0, rank_zero_iff_forall_zero, Cardinal.one_lt_aleph0, MonoidAlgebra.cardinalMk_of_infinite, HahnSeries.cardSupp_single_le, Ordinal.card_iSup_Iio_le_sum_card, Ordinal.card_one, Cardinal.mk_vector, Cardinal.ofENat_le_aleph0, Cardinal.lift_zero, Cardinal.aleph0_power_aleph0, Cardinal.le_aleph0_iff_set_countable, Cardinal.natCast_mul_inj, Cardinal.card_le_of_finset, Cardinal.toNat_mul, Matroid.isRkFinite_iff_cRk_lt_aleph0, rank_eq_card_basis, Cardinal.mk_list_eq_sum_pow, LinearMap.le_rank_iff_exists_linearIndependent, Cardinal.sum_le_mk_mul_iSup, IntermediateField.relrank_mul_rank_top, IntermediateField.relrank_eq_one_iff, rank_map_le, Cardinal.mk_fin, rank_eq_one, LinearMap.lift_rank_comp_le_right, Module.le_rank_iff_exists_linearMap, Ordinal.isInitialIso_symm_apply_coe, Cardinal.mk_monotone, Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free, Cardinal.mk_finsupp_lift_of_infinite, Cardinal.succ_natCast, Submodule.spanRank_toENat_eq_iInf_encard, LinearMap.rank_eq_of_surjective, Cardinal.ofNat_lt_lift_iff, Cardinal.IsStrongLimit.aleph0_le, ZFSet.card_singleton, Order.le_cof, Ordinal.card_zero, Cardinal.mk_le_one_iff_set_subsingleton, Cardinal.mk_le_aleph0_iff, Cardinal.mk_eq_nat_iff, Cardinal.isNormal_preAleph, Cardinal.bddAbove_ord_image_iff, Subfield.cardinalMk_closure_le_max, Cardinal.toENat_eq_zero, Cardinal.mul_eq_left_iff, rank_bot, Cardinal.mul_natCast_le_mul_natCast, FixedPoints.rank_le_card, algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded, Matroid.IsBase.cardinalMk_le_cRank, Cardinal.toENat_eq_ofNat, Cardinal.power_add, ModularForm.levelOne_neg_weight_rank_zero, Cardinal.lift_lt_ofNat_iff, Cardinal.le_mk_iff_exists_set, Cardinal.preAleph_nat, AddMonoidAlgebra.cardinalMk_lift_of_fintype, Cardinal.lift_iInf, Cardinal.aleph0_le_beth, LinearMap.rank_diagonal, rank_matrix_module, Ordinal.cof_eq_one_iff_is_succ, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, Cardinal.lift_succ, Field.sepDegree_self, Cardinal.ofENat_mono, Cardinal.le_range_of_union_finset_eq_top, Ordinal.card_le_card, trdeg_lt_aleph0, Algebraic.cardinalMk_le_max, Subfield.relrank_eq_one_of_le, Cardinal.ofENat_le_ofENat_of_le, Subfield.relrank_mul_rank_top, trdeg_eq_zero, Cardinal.mk_le_aleph0, Cardinal.mk_subset_ge_of_subset_image_lift, Computability.Encoding.card_le_card_list, Module.one_lt_rank_of_one_lt_finrank, Cardinal.zero_le, Cardinal.continuum_mul_self, Cardinal.prod_const, Matroid.cRank_eq_iSup_cardinalMk_indep, rank_le_of_injective_injective, Ordinal.card_sInf_range_compl_le_lift, Cardinal.mk_eq_two_iff', Cardinal.mk_emptyCollection, Nat.count_le_cardinal, Module.rank_pos_iff_of_free, AddLocalization.cardinalMk_le, Cardinal.nsmul_lt_aleph0_iff_of_ne_zero, Algebra.IsAlgebraic.cardinalMk_le_max, rank_mul_rank, Subfield.relrank_top_left, Cardinal.mk_div_le, Ordinal.cof_lsub_le_lift, Cardinal.ord_eq_zero, rank_subsingleton', Cardinal.preAleph_le_aleph, FirstOrder.Language.card_eq_card_functions_add_card_relations, Cardinal.mk_union_add_mk_inter, Cardinal.liftInitialSeg_toFun, Field.Emb.Cardinal.two_le_deg, IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic, Module.Basis.le_span, Submodule.rank_quotient_add_rank, Submodule.rank_le_spanRank, IsPurelyInseparable.sepDegree_eq_one, Filter.mem_cardinaleGenerate_iff, FirstOrder.Language.Sentence.realize_cardGe, Field.instNeZeroInsepDegree, Cardinal.mk_iUnion_le_sum_mk_lift, rank_submodule_le_one_iff, Ordinal.cof_blsub_le_lift, Cardinal.aleph_one_le_continuum, Module.one_le_rank_iff, Cardinal.lift_monotone, MvPolynomial.rank_R, HahnSeries.cardSupp_truncLT_le, Matrix.cRank_le_card_height, Module.rank_bot_le_rank_of_isScalarTower, Cardinal.toENatAux_eq_nat, Ordinal.card_le_preAleph, Cardinal.ofENat_lt_aleph0, Cardinal.aleph_mul_aleph0, Ordinal.card_omega0_opow, CommSemiring.rank_self, Cardinal.le_one_iff_subsingleton, Cardinal.zero_power_le, HahnSeries.cardSupp_one_le, Field.nonempty_iff, Cardinal.isInaccessible_def, Cardinal.mk_le_iff_forall_finset_subset_card_le, Submodule.spanRank_range_le, Cardinal.preBeth_one, Cardinal.instNontrivial, lift_trdeg_le_of_injective, Field.rank_mul_sepDegree_of_isSeparable, rank_range_le, Submodule.rank_le, Ordinal.card_sInf_range_compl_le, Matrix.cRank_toNat_eq_rank, Cardinal.mk_union_le_aleph0, HahnSeries.cardSupp_map_le, Submodule.spanRank_span_le_card, Cardinal.toENat_lt_natCast_iff, Cardinal.card_le_iff, natCast_le_rank_iff, Cardinal.small_Iio, Cardinal.nat_lt_aleph0, Cardinal.natCast_add_one_le_iff, LinearIndependent.cardinal_le_rank, Cardinal.mk_setProd, Cardinal.mk_strictMonoOn, Matroid.cRk_le_cardinalMk, Ordinal.IsNormal.cof_le, Filter.mem_cocardinal, Cardinal.mul_natCast_strictMono, lift_rank_le_of_surjective_injective, Cardinal.cast_toNat_eq_iff_lt_aleph0, Cardinal.toENatAux_nat, FreeAlgebra.cardinalMk_le_max, Cardinal.nat_lt_continuum, Algebra.IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth, Cardinal.aleph_add_aleph, Submodule.LinearDisjoint.rank_inf_le_one_of_flat, LinearEquiv.mem_dilatransvections_iff_rank, Cardinal.mk_biUnion_le_lift, HahnSeries.mem_cardSuppLTSubring, Cardinal.nat_eq_ofENat, Module.rank_top_le_rank_of_isScalarTower, Cardinal.preAleph_omega0, Cardinal.toENat_lift, Matrix.cRank_toNat_eq_finrank, rank_le_of_surjective_injective, MonoidAlgebra.cardinalMk_lift_of_infinite, Cardinal.ofNat_mul_aleph0, Subalgebra.LinearDisjoint.rank_sup_of_free, Cardinal.beth_succ, Cardinal.aleph0_add_continuum, Cardinal.continuum_lt_lift, Ordinal.nat_le_card, Cardinal.toNat_monotoneOn, Submodule.le_spanRank_restrictScalars, WType.cardinalMk_le_max_aleph0_of_finite', Matroid.cRk_mono, Cardinal.instNoMaxOrder, Cardinal.lift_le_nat_iff, Cardinal.toENat_le_ofNat, Cardinal.lt_omega_iff_card_lt, Cardinal.mk_toNat_eq_card, Cardinal.instCanLiftENatOfENatLeAleph0, Cardinal.nat_mul_continuum, strongRankCondition_iff_forall_rank_lt_aleph0, Cardinal.lift_lt_ofENat, Cardinal.le_preAleph_ord, Cardinal.aleph1_le_lift, Cardinal.lt_univ, Module.le_rank_iff, FirstOrder.Language.card_functions_sum_skolem₁_le, Module.rank_linearMap, IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right, WType.cardinalMk_eq_sum_lift, Ordinal.card_le_one, Cardinal.mk_univ_quaternionAlgebra, Cardinal.add_lt_aleph0_iff, Module.lift_rank_bot_le_lift_rank_of_isScalarTower, Cardinal.aleph0_le, Cardinal.mk_embedding_eq_zero_iff_lift_lt, LinearRecurrence.solSpace_rank, Cardinal.lift_power_sum, Module.finrank_eq_card_basis', Cardinal.infinite_iff, Ordinal.sSup_ord, Cardinal.mk_iUnion_le_sum_mk, FirstOrder.Language.Substructure.lift_card_closure_le_card_term, Cardinal.IsRegular.aleph0_le, Cardinal.le_aleph_ord, AddMonoidAlgebra.cardinalMk_of_infinite', Ordinal.IsInitial.card_lt_card, RCLike.rank_le_two, TensorAlgebra.rank_eq, Cardinal.lt_one_iff_zero, Cardinal.continuum_mul_nat, Cardinal.nat_coe_dvd_iff, Cardinal.IsInaccessible.nat_lt, Cardinal.mk_freeMonoid, Cardinal.mk_bounded_set_le, cardinalInterFilter_aleph_one_iff, Ordinal.nat_lt_card, univLE_iff_cardinal_le, LinearMap.rank_comp_le_left, not_small_cardinal, Cardinal.aleph0_le_mk_iff, Module.le_rank_iff_exists_finset, Submodule.spanRank_finite_iff_fg, Matrix.cRank_le_card_width, ModularForm.levelOne_weight_zero_rank_one, MeasurableSpace.cardinal_generateMeasurableRec_le, Ordinal.card_eq_zero, Cardinal.prod_eq_zero, Cardinal.one_le_ofENat, Cardinal.ofNat_mul_continuum, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, Cardinal.sum_nat_eq_add_sum_succ, Cardinal.mk_image_le, HahnSeries.cardSupp_neg_le, Cardinal.aleph_le_aleph, Cardinal.ord_eq_one, WType.cardinalMk_le_max_aleph0_of_finite, Ordinal.cof_le_card, Cardinal.ofNat_le_aleph0, Cardinal.small_Icc, Cardinal.one_le_iff_ne_zero, InnerProductSpace.rank_rankOne, Cardinal.IsStrongLimit.isSuccLimit, trdeg_add_eq, HahnSeries.mem_cardSuppLTAddSubgroup, Cardinal.mk_coe_finset, Algebra.rank_le_of_surjective_injective, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank, rank_pos_iff_nontrivial, Cardinal.lift_lt_univ', Cardinal.mk_list_eq_max, lift_rank_add_lift_rank_le_rank_prod, Cardinal.univ_pos, Matroid.IsBasis.cardinalMk_le_cRk, FirstOrder.Language.order.card_eq_one, Ordinal.le_cof_iff_blsub, Cardinal.mk_freeAddGroup, Cardinal.IsInaccessible.aleph0_lt, Ordinal.card_le_preBeth, QuadraticAlgebra.rank_eq_two, Cardinal.ofENat_eq_zero, Filter.frequently_cocardinal, Cardinal.beth_le_beth, IntermediateField.rank_adjoin_eq_one_iff, nonempty_embedding_to_cardinal, LinearMap.lift_rank_le_of_injective, Ordinal.card_iSup_Iio_le_card_mul_iSup, Cardinal.ofENat_add, rank_submodule_le_one_iff', Cardinal.preBeth_zero, Algebra.rank_le_of_injective_injective, Module.rank_pos_of_free, Cardinal.mk_finsupp_nat, Cardinal.ord_aleph, IntermediateField.rank_top, OrdinalApprox.lfpApprox_ord_eq_lfp, LinearMap.rank_le_of_injective, LinearMap.lift_rank_eq_of_surjective, IsClosed.two_pow_mk_le_two_pow_mk_dense, Cardinal.mul_def, Submodule.rank_mono, Ordinal.card_lt_nat, Cardinal.powerlt_zero, AddMonoidAlgebra.cardinalMk_lift_of_infinite, Cardinal.mul_ciSup, Module.lt_rank_of_lt_finrank, Cardinal.mk_image2_le, Cardinal.bddAbove_range, HahnSeries.coe_cardSuppLTAddSubgroup, AddMonoidAlgebra.cardinalMk_of_fintype, Field.rank_mul_insepDegree_of_isPurelyInseparable, Ordinal.one_lt_card, Cardinal.ofENat_lt_ofENat_of_lt, ZFSet.card_pair_of_ne, rank_quotient_add_rank_of_isDomain, Cardinal.lift_mk_fin, Cardinal.zero_eq_lift_iff, Cardinal.lift_le_ofNat_iff, Cardinal.ciSup_mul, Cardinal.ord_le, Ordinal.card_ofNat, Cardinal.ord_zero, Cardinal.uncountable, lift_trdeg_le_of_surjective, Cardinal.mk_preimage_of_subset_range, IntermediateField.relrank_dvd_of_le_left, Cardinal.one_power, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right, OrdinalApprox.lfpApprox_ord_mem_fixedPoint, Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, Ordinal.cof_succ, Set.Subsingleton.cardinalMk_le_one, Cardinal.mk_perm_eq_two_power, rank_eq_zero_iff_isTorsion, IntermediateField.cardinalMk_adjoin_le, Matroid.cRank_le_iff, Cardinal.prod_const', IntermediateField.relrank_top_left, Cardinal.mk_freeAddMonoid, rank_tensorProduct, Cardinal.isRegular_aleph_succ, Cardinal.continuum_pos, Cardinal.ord_le_ord, Cardinal.beth_mono, rank_le_of_injective_injectiveₛ, Cardinal.mk_equiv_of_eq, Matroid.Indep.cardinalMk_le_isBasis, Cardinal.ofNat_lt_aleph0, Cardinal.preBeth_le_beth, Cardinal.powerlt_mono_left, Cardinal.nat_eq_lift_iff, Cardinal.powerlt_min, Cardinal.toNat_rightInverse, Cardinal.le_mk_diff_add_mk, Cardinal.power_nat_le_max, Cardinal.ofENat_injective, Cardinal.aleph0_lt_mk_iff, Cardinal.aleph1_lt_lift, Cardinal.toNat_strictMonoOn, Cardinal.continuum_add_self, Ordinal.card_add, MvPolynomial.cardinalMk_eq_one, Cardinal.mk_equiv_eq_zero_iff_ne, AddOreLocalization.cardinalMk_le_lift_cardinalMk_of_addCommute, Cardinal.mk_sum_compl, Cardinal.sum_add_distrib', Algebra.IsAlgebraic.lift_cardinalMk_le_max, Cardinal.ofENat_eq_one, Cardinal.preAleph_limit, LinearIndependent.cardinal_le_rank', iSupIndep.subtype_ne_bot_le_rank, Cardinal.isNormal_aleph, Cardinal.continuum_mul_aleph0, cardinalMk_eq_cardinalMk_field_pow_rank, Computability.FinEncoding.card_le_aleph0, QuaternionAlgebra.rank_eq_four, Cardinal.omega0_le_ord, Ideal.spanRank_map_le, trdeg_add_le, Cardinal.ofENat_mul, Cardinal.card_lt_card_of_left_finite, Cardinal.instCharZero, MonoidAlgebra.cardinalMk_of_infinite', linearIndependent_bounded_of_finset_linearIndependent_bounded, linearIndependent_le_basis, Cardinal.lift_iSup_le_sum, Complex.rank_real_complex', Cardinal.mk_subtype_le, rank_eq_one_iff, ZFSet.lift_card_iUnion_le_sum_card, Cardinal.ofENat_le_ofENat, Cardinal.card_typein_lt, rank_le_card, Cardinal.add_one_le_succ, Cardinal.ofNat_lt_ofENat, Cardinal.card_typein_toType_lt, Cardinal.is_prime_iff, Cardinal.mk_set_eq_one_iff, Cardinal.lift_eq_aleph1, rank_span_finset_le, le_rank_iff_exists_linearIndependent, Cardinal.mk_union_of_disjoint, HahnSeries.cardSupp_div_le, Cardinal.small_Ioo, IntermediateField.sepDegree_bot, Cardinal.sum_le_lift_mk_mul_iSup, Cardinal.toNat_lift, HahnSeries.cardSupp_mul_single_le, Ordinal.cof_le_of_isNormal, Cardinal.mk_powerset, Ordinal.cof_lsub_def_nonempty, Cardinal.canonicallyOrderedAdd, Cardinal.natCast_lt_aleph0, Cardinal.IsInaccessible.pos, Cardinal.mk_fintype, OrdinalApprox.gfpApprox_ord_eq_gfp, Cardinal.isUnit_iff, Cardinal.mk_eq_zero_iff, ZFSet.lift_card_range_le, Cardinal.lift_lt, Cardinal.mk_freeRing, Cardinal.mul_natCast_inj, Cardinal.lt_wf, Module.Invertible.rank_eq_one, Cardinal.toNat_eq_one, Cardinal.aleph0_lt_mk, Cardinal.preBeth_lt_preBeth, Cardinal.mk_range_le, Ordinal.card_opow_le_of_omega0_le_right, Cardinal.add_nat_le_add_nat_iff, Cardinal.aleph0_add_ofNat, trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial, Cardinal.instWellFoundedLT, Cardinal.mul_mk_eq_max, Cardinal.ord_lt_omega0, Cardinal.sInf_eq_zero_iff, HahnSeries.cardSupp_single_mul_le, Subfield.relrank_mul_relrank_eq_inf_relrank, Cardinal.toENatAux_gc, Cardinal.aleph0_le_lift, Cardinal.toNat_toENat, Cardinal.aleph_max, Cardinal.IsStrongLimit.isSuccPrelimit, Cardinal.le_lift_iff, Cardinal.ofNat_add_continuum, Cardinal.isSuccLimit_aleph0, Cardinal.ord_preAleph, IntermediateField.rank_bot, OreLocalization.cardinalMk_le_max, OreLocalization.cardinalMk_le_lift_cardinalMk_of_commute, Cardinal.mk_strictMono, Submodule.rank_eq_zero, Cardinal.lift_eq_ofNat_iff, Ordinal.card_opow_omega0, Ordinal.cof_eq_sInf_lsub, Cardinal.small_Ioc, Subalgebra.LinearDisjoint.rank_eq_one_of_commute_of_flat_of_self_of_inj, Cardinal.powerlt_le, Ordinal.aleph0_le_card, Cardinal.mk_quot_le, Cardinal.addRightMono, Cardinal.le_mul_left, IntermediateField.relfinrank_eq_toNat_relrank, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_of_inj, rank_punit, Cardinal.preAleph_max, Cardinal.beth_pos, Module.finrank_eq_rank, HasRankNullity.rank_quotient_add_rank, Cardinal.type_cardinal, Cardinal.preBeth_le_preBeth, Subfield.relrank_inf_mul_relrank, Field.lift_rank_mul_lift_insepDegree_of_isPurelyInseparable, IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right, Cardinal.ofENat_eq_nat, Submodule.IsLattice.rank_of_pi, Cardinal.mk_abelianization_le, Subfield.relfinrank_eq_toNat_relrank, Cardinal.aleph0_mul_continuum, toENat_rank_span_set, Matroid.cRk_le_iff, Cardinal.mk_finsupp_of_fintype, Cardinal.eq_one_iff_unique, Submodule.finrank_eq_rank, Matroid.Indep.cardinalMk_le_cRank, Cardinal.nat_lt_lift_iff, Cardinal.power_one, Set.Countable.le_aleph0, Cardinal.mk_toNat_of_infinite, HahnSeries.cardSupp_zero, MeasurableSpace.cardinal_measurableSet_le_continuum, IsClosed.two_pow_mk_lt_continuum, Algebra.lift_rank_le_of_injective_injective, Module.rank_zero_iff_of_free, IntermediateField.relrank_dvd_rank_top_of_le, Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial, Ordinal.card_le_nat, Cardinal.toENat_strictMonoOn, AlgebraicIndependent.cardinalMk_le_trdeg, Cardinal.not_isSuccLimit_natCast, Cardinal.lift_two, Polynomial.cardinalMk_eq_max, rank_span_le, Cardinal.aleph0_add_aleph0, rank_submodule_eq_one_iff, Matroid.Indep.cardinalMk_le_isBasis', Cardinal.preAleph_le_of_isSuccPrelimit, Cardinal.range_aleph, IntermediateField.relrank_dvd_rank_bot, Cardinal.cantor, IsAlgClosed.cardinal_le_max_transcendence_basis', WType.cardinalMk_eq_sum, Cardinal.beth_limit, Cardinal.lift_lt_univ, Cardinal.power_zero, Matroid.rankInfinite_iff_aleph0_le_cRank, Cardinal.aleph0_le_preAleph, LinearMap.rank_le_range, Cardinal.sum_const', Cardinal.preAleph_succ, Cardinal.mk_arrow, Cardinal.ofNat_le_ofENat, Cardinal.mk_biUnion_le, Cardinal.lt_aleph0_iff_subtype_finite, Cardinal.lt_lift_iff, Submodule.spanRank_toENat_eq_iInf_finset_card, Subalgebra.rank_sup_eq_rank_right_mul_rank_of_free, Cardinal.aleph0_le_add_iff, trdeg_pos, Subfield.relrank_inf_mul_relrank_of_le, rank_matrix_module', Subfield.relrank_dvd_rank_top_of_le, FirstOrder.Language.Term.card_sigma, Cardinal.aleph_one_le_lift, Filter.hasBasis_cocardinal, Cardinal.le_preBeth_ord, Cardinal.mk_bounded_subset_le, OrdinalApprox.exists_gfpApprox_eq_gfpApprox, collinear_iff_rank_le_one, Cardinal.aleph0_lt_univ, Cardinal.preBeth_succ, Cardinal.nat_succ, FirstOrder.Language.card_empty, Cardinal.lift_natCast, Cardinal.sum_le_iSup_lift, Ordinal.cof_type_le, Nat.cast_card, Module.mk_finrank_eq_card_basis, Cardinal.mk_le_mk_of_subset, Cardinal.not_injective_limitation_set, Cardinal.mk_iUnion_le_lift, Cardinal.mk_bool, MeasurableSpace.cardinal_generateMeasurable_le_continuum, Cardinal.continuum_toENat, Cardinal.ord_nat, Cardinal.lift_le_one_iff, Field.Emb.Cardinal.deg_lt_aleph0, continuum_le_cardinal_of_nontriviallyNormedField, Cardinal.natCast_mul_strictMono, Ordinal.ofNat_lt_card, Cardinal.add_mk_eq_max, Cardinal.lift_le_aleph1, Cardinal.mk_eq_two_iff, Cardinal.gc_ord_card, Cardinal.le_mul_right, AddMonoidAlgebra.cardinalMk_lift_of_infinite', Cardinal.mk_set_le, Ordinal.card_le_beth, ZFSet.card_union_le, Cardinal.mk_finset_of_fintype, IntermediateField.LinearDisjoint.rank_sup, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj, FirstOrder.Language.Theory.exists_large_model_of_infinite_model, LinearMap.lift_rank_range_add_rank_ker, Cardinal.toNat_injOn, Cardinal.succ_def, IntermediateField.rank_sup_le_of_isAlgebraic, Cardinal.mk_eq_nat_iff_finset, rank_matrix', Ordinal.iSup_ord, IntermediateField.relrank_eq_one_of_le, Cardinal.mul_lt_aleph0_iff, Cardinal.preAleph_zero, Ordinal.card_succ, Cardinal.ord_one, Cardinal.lt_aleph0_iff_finite, LinearMap.rank_zero, MonoidAlgebra.cardinalMk_lift_of_fintype, Cardinal.mk_finsupp_lift_of_fintype, Filter.eventually_cocardinal, Ordinal.aleph0_le_cof, Ordinal.card_omega, Module.rank_self, Submodule.rank_add_le_rank_add_rank, Cardinal.ofENat_lt_ofENat, Field.sepDegree_mul_insepDegree, Cardinal.sInf_empty, Submodule.spanRank_sup_le_sum_spanRank, Cardinal.continuum_add_aleph0, Cardinal.isSuccLimit_iff, Cardinal.mk_freeGroup, Cardinal.lift_aleph, IntermediateField.rank_eq_one_iff, Matroid.rankFinite_iff_cRank_lt_aleph0, rank_quotient_add_rank_le, Ordinal.ofNat_le_card, cardinal_lt_aleph0_of_finiteDimensional, Cardinal.ofENat_nat, Cardinal.continuum_le_lift, IntermediateField.adjoin_rank_le_of_isAlgebraic_right, Cardinal.not_isStrongLimit_zero, Cardinal.small_iff_lift_mk_lt_univ, Cardinal.prod_eq_of_fintype, Ordinal.card_opow_eq_of_omega0_le_right, Field.insepDegree_self, Cardinal.ofENat_strictMono, rank_matrix, Cardinal.mk_eq_nat_iff_fintype, Cardinal.toENatAux_zero, MeasurableSpace.cardinal_measurableSet_le, Field.instNeZeroSepDegree, Cardinal.sum_add_distrib, Cardinal.lift_two_power, Cardinal.two_le_iff, MeasurableSpace.cardinal_generateMeasurable_le, Submodule.LinearDisjoint.rank_le_one_of_flat_of_self, Cardinal.aleph0_le_aleph, HahnSeries.mem_cardSuppLTAddSubmonoid, Ordinal.zero_lt_card, Cardinal.isOrderedRing, Ordinal.IsInitial.card_le_card, Cardinal.preAleph_le_preAleph, Cardinal.addLeftMono, ZFSet.card_insert_le, Cardinal.one_lt_two, Cardinal.sum_le_lift_mk_mul_iSup_lift, IsAlgClosed.cardinal_le_max_transcendence_basis, lift_trdeg_add_eq, Ordinal.card_eq_nat, Matroid.cRk_inter_add_cRk_union_le, Ordinal.card_eq_one, Ideal.rank_pow_quot_aux, Cardinal.toENat_eq_top, ZFSet.card_insert, Cardinal.mk_perm_eq_self_power, Cardinal.toNat_eq_one_iff_unique, Cardinal.add_one_inj, IsLocalization.lift_cardinalMk_le, Cardinal.small_Iic, IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left, Cardinal.mk_surjective_eq_zero_iff, Cardinal.mk_mul_le, Cardinal.ofENat_add_aleph0, Ordinal.lift_card_sInf_compl_le, Cardinal.bddAbove_iff_small, Cardinal.one_lt_iff_nontrivial, Cardinal.mk_set, Cardinal.two_le_iff', Cardinal.aleph0_lt_aleph_one, IntermediateField.relrank_inf_mul_relrank_of_le, Cardinal.one_lt_ofENat, Subalgebra.rank_sup_le_of_free, rank_quotient_le, Ideal.rank_pow_quot, Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self, Cardinal.preBeth_limit, LinearIndependent.lt_aleph0_of_finiteDimensional, Cardinal.preAleph_lt_preAleph, Module.rank_eq_ofNat_iff_finrank_eq_ofNat, Module.rank_le_one_iff_top_isPrincipal, Set.cast_ncard, Cardinal.aleph_mul_aleph, Ordinal.card_mul, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj, rank_span_of_finset, Cardinal.ofENat_lt_nat, IntermediateField.adjoin_rank_le_of_isAlgebraic, Cardinal.continuum_power_aleph0, Cardinal.beth_strictMono, Cardinal.nat_is_prime_iff, Cardinal.toENatAux_eq_zero, Cardinal.one_lt_lift_iff, Ordinal.card_opow_le_of_omega0_le_left, Cardinal.isRegular_aleph_one, Cardinal.ofENat_le_one, LinearIndependent.aleph0_le_rank, Cardinal.zero_power, Algebra.IsSeparable.insepDegree_eq, Matroid.Spanning.cRank_le_cardinalMk, Algebraic.aleph0_le_cardinalMk_of_charZero, Cardinal.ofENat_pos, Cardinal.lift_mk_le_lift_mk_of_injective, Cardinal.mk_Prop, Cardinal.noZeroDivisors, FirstOrder.Language.Term.card_le, rank_fin_fun, Cardinal.lift_ofNat, Cardinal.lift_le_sum, Cardinal.lift_le_aleph_one, Cardinal.toENat_le_natCast_iff, Set.toENat_cardinalMk, Cardinal.ofENat_mul_aleph0, Cardinal.nsmul_lt_aleph0_iff, Cardinal.mul_power, cardinalMk_algHom_le_rank, Module.rank_eq_one_iff_finrank_eq_one, Ordinal.card_opow_eq_of_omega0_le_left, Filter.cocardinal_inf_principal_neBot_iff, Cardinal.power_sum, Cardinal.ord_injective, Cardinal.enat_gc, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj, IntermediateField.relrank_mul_relrank, LinearIndependent.lt_aleph0_of_finite, Algebraic.cardinalMk_le_mul, HahnSeries.cardSupp_mono, Cardinal.le_aleph0_iff_subtype_countable, Cardinal.aleph0_le_mul_iff', Matrix.cRank_zero, Cardinal.toENatAux_le_nat, Cardinal.continuum_add_ofNat, Cardinal.toENat_le_nat, LinearMap.rank_le_of_surjective, Ordinal.card_preOmega, IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left, Cardinal.add_mk_eq_max', Cardinal.mk_plift_false, Cardinal.ciSup_mul_ciSup, Cardinal.lift_mk_le', Order.cof_le, Cardinal.lift_sInf, OrdinalApprox.exists_lfpApprox_eq_lfpApprox, Cardinal.one_eq_lift_iff, MvPolynomial.cardinalMk_le_max_lift, IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, Cardinal.toNat_eq_zero, rank_real_of_complex, Cardinal.mk_sum, Cardinal.powerlt_succ, Cardinal.lift_mul, Cardinal.continuum_add_nat, IntermediateField.relrank_self, HahnSeries.cardSupp_add_le, rank_pos_iff_exists_ne_zero, Cardinal.mk_pempty, max_aleph0_card_le_rank_fun_nat, FreeAlgebra.cardinalMk_le_max_lift, Filter.frequently_cocardinal_mem, Cardinal.aleph1_eq_lift, Field.finSepDegree_eq, IntermediateField.lift_cardinalMk_adjoin_le, Module.finrank_eq_rank', Cardinal.isSuccPrelimit_aleph0, Cardinal.card_surjective, Ordinal.card_nat, Cardinal.mk_add_le, Cardinal.canLiftCardinalNat, Cardinal.natCast_mul_le_natCast_mul, Cardinal.aleph0_lt_lift, Cardinal.add_nat_inj, Cardinal.lift_lt_aleph0, Cardinal.lt_aleph0_of_finite, rank_prod', Subalgebra.rank_eq_one_iff, Ordinal.sInf_compl_lt_ord_succ, Cardinal.ord_strictMono, Cardinal.powerlt_aleph0_le, Cardinal.mk_insert, Cardinal.toENat_comp_ofENat, Cardinal.mk_quotient_le, Submodule.rank_le_one_iff_isPrincipal, MonoidAlgebra.cardinalMk_lift_of_infinite', Cardinal.preAleph_le_preBeth, Cardinal.mk_bounded_set_le_of_infinite, Field.finInsepDegree_def', IntermediateField.rank_sup_le, Cardinal.ord_lt_ord, Subfield.relrank_eq_one_iff, Cardinal.mk_set_eq_nat_iff_finset, FirstOrder.Language.card_withConstants, Cardinal.preAleph_pos, Cardinal.beth_lt_beth, Set.Finite.lt_aleph0, Cardinal.add_eq_left_iff, Cardinal.small_Ico, Cardinal.aleph0_pos, LinearMap.rank_comp_le, Matrix.cRank_submatrix_le, ZFSet.card_mono, Cardinal.mk_finsupp_of_infinite, Cardinal.isSuccPrelimit_zero, Cardinal.mk_set_eq_zero_iff, Cardinal.ofENat_toENat_le, Cardinal.omega0_lt_ord, rank_add_rank_le_rank_prod, IntermediateField.relrank_bot_right, IsClosed.mk_lt_continuum, Cardinal.succ_zero, Ordinal.card_le_card_vonNeumann, Cardinal.bddAbove_of_small, Cardinal.lift_one, Ordinal.cof_ord_le, rank_add_rank_split, Cardinal.toENat_le_one, Cardinal.zero_powerlt, Cardinal.lt_aleph0, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj, Algebra.SubmersivePresentation.rank_kaehlerDifferential, Cardinal.mk_le_of_injective, Cardinal.range_natCast, Function.Embedding.cardinal_le, Cardinal.canLiftCardinalType, ModuleCat.free_shortExact_rank_add, Cardinal.zero_eq_ofENat, Cardinal.mk_singleton, Cardinal.toENat_injOn, LinearIndepOn.encard_le_toENat_rank, rank_eq_zero_iff, trdeg_subsingleton, Cardinal.toENat_eq_nat, Cardinal.mk_cardinal, ZFSet.card_empty, Cardinal.two_power_aleph0, Polynomial.cardinalMk_le_max, Cardinal.aleph0_toNat, Submodule.spanRank_eq_zero_iff_eq_bot, basis_le_span', rank_quotient_add_rank_of_divisionRing, rank_pos, Cardinal.aleph_eq_preAleph, Cardinal.mul_natCast_lt_mul_natCast, Cardinal.mk_quaternion, Cardinal.ofNat_eq_lift_iff, ZFSet.card_powerset, rank_finsupp', Field.lift_rank_mul_lift_sepDegree_of_isSeparable, Cardinal.nat_le_ofENat, Cardinal.mk_multiset_of_isEmpty, trdeg_le_of_surjective, infinite_basis_le_maximal_linearIndependent', Cardinal.ofENat_toENat_eq_self, Cardinal.toNat_natCast, Cardinal.preBeth_strictMono, Algebra.cardinalMk_adjoin_le, Cardinal.sum_le_iSup, MonoidAlgebra.cardinalMk_of_fintype, Cardinal.isNormal_beth, AlgebraicIndependent.lift_cardinalMk_le_trdeg, Cardinal.mk_eq_one, Cardinal.lift_mk_le_lift_mk_of_surjective, CountableInterFilter.toCardinalInterFilter, Localization.cardinalMk_le, Cardinal.aleph_one_eq_lift, Cardinal.mk_surjective_eq_zero_iff_lift, Field.insepDegree_top_le_insepDegree_of_isScalarTower, Cardinal.one_le_lift_iff, Cardinal.iInf_eq_zero_iff, Cardinal.aleph_toENat, FirstOrder.Language.card_functions_sum, LinearMap.rank_add_le, Cardinal.preBeth_mono, rank_zero_iff, Cardinal.lift_lt_continuum, Cardinal.countable_iff_lt_aleph_one, IntermediateField.adjoin_rank_le_of_isAlgebraic_left, Cardinal.card_le_of_le_ord, hasCardinalLT_iff_cardinal_mk_lt, Ordinal.cof_eq_zero, IntermediateField.insepDegree_bot, rank_fun, Cardinal.sum_pow_eq_max_aleph0, Cardinal.add_mk_eq_self, Cardinal.aleph0_mul_ofENat, Cardinal.mk_diff_add_mk, lift_rank_range_le, Ordinal.card_lt_aleph0, lift_trdeg_add_le, Cardinal.aleph0_mul_mk_eq, Cardinal.IsRegular.nat_lt, Filter.cardinalInterFilter_inf, linearIndependent_le_span'', FirstOrder.Language.card_sum, cardinalMk_algHom, rank_fun', Cardinal.lift_le_continuum, Cardinal.isNormal_preBeth, Cardinal.mk_image_le_lift, Cardinal.aleph_limit, Cardinal.mk_arrow_eq_zero_iff, Cardinal.mk_lt_aleph0, IntermediateField.rank_bot_mul_relrank, lift_rank_le_of_injective_injective, Ordinal.cof_lsub_le, Cardinal.mk_lt_aleph0_iff, Ordinal.cof_bsup_le_lift, Cardinal.nat_le_lift_iff, Cardinal.isNormal_ord, continuum_le_cardinal_of_module, Subfield.relrank_mul_relrank, Ordinal.card_lt_ofNat, le_rank_iff_exists_linearIndependent_finset, Cardinal.aleph0_mul_aleph, Cardinal.mk_union_le, IsClosed.mk_lt_two_pow_mk_dense, Cardinal.lift_lt_aleph1, lift_rank_le_of_injective_injectiveₛ, rank_fun_eq_lift_mul, Ideal.height_le_spanRank_toENat, rank_le_of_isSMulRegular, IsTranscendenceBasis.lift_cardinalMk_eq_max_lift, IsTranscendenceBasis.lift_rank_eq_max_lift, Submodule.rank_sup_add_rank_inf_eq, MvRatFunc.rank_eq_max_lift, Cardinal.toNat_pos, Cardinal.lift_strictMono, Cardinal.natCast_eq_toENat_iff, Cardinal.ofENat_le_nat, MvPolynomial.cardinalMk_le_max, rank_le_one_iff, Cardinal.lift_add, Cardinal.mk_freeCommRing, FreeAlgebra.cardinalMk_eq_one, Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential, Cardinal.one_le_iff_pos, Cardinal.mk_freeAbelianGroup, IntermediateField.relrank_inf_mul_relrank, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left, Cardinal.lift_power, HahnSeries.cardSupp_sub_le, infinite_basis_le_maximal_linearIndependent, Cardinal.ord_le_omega0, Cardinal.aleph_one_lt_lift, Cardinal.aleph0_mul_nat, Ordinal.le_cof_iff_lsub, Cardinal.toENat_nat, Cardinal.IsRegular.pos, Cardinal.lift_eq_nat_iff, HahnSeries.cardSupp_hsum_powers_le, Cardinal.mk_univ_quaternion, Cardinal.add_le_max, Cardinal.mk_preimage_of_injective_lift, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj, Cardinal.isInaccesible_def, Cardinal.toNat_ne_zero, Cardinal.ofNat_add_aleph0, linearIndependent_le_infinite_basis, Matroid.toENat_cRank_eq, Cardinal.mk_plift_true, Matroid.Indep.cardinalMk_le_isBase, Matroid.cRk_le_of_subset, Cardinal.mk_empty, Field.sepDegree_le_rank, Cardinal.preBeth_pos, Ordinal.card_opow_le, OreLocalization.cardinalMk_le, Cardinal.lt_univ', Cardinal.preBeth_nat, Cardinal.mk_finsupp_lift_of_infinite', Cardinal.lift_eq_zero, Cardinal.mul_lt_aleph0_iff_of_ne_zero, Cardinal.ofENat_zero, IsLocalization.cardinalMk_le, rank_tensorProduct', IntermediateField.relrank_mul_relrank_eq_inf_relrank, Cardinal.mk_preimage_of_injective, Cardinal.mk_equiv_of_lift_eq, Module.rank_lt_aleph0, Ordinal.cof_bsup_le, Cardinal.mem_range_aleph_iff, trdeg_eq_zero_iff, ZFSet.card_image_le, Cardinal.mk_embedding_eq_zero_iff_lt, Cardinal.ord_mono, FirstOrder.Ring.card_ring, Cardinal.aleph_lt_aleph, Algebra.lift_rank_le_of_surjective_injective, Subalgebra.bot_eq_top_iff_rank_eq_one, rank_prod, rank_le, Cardinal.power_def, Cardinal.zero_lt_lift_iff, Cardinal.nat_power_aleph0, Cardinal.ofENat_one, Cardinal.mul_le_max, Cardinal.nat_lt_univ, Matroid.IsBasis'.cardinalMk_le_cRk, Subalgebra.LinearDisjoint.rank_eq_one_of_flat_of_self_of_inj, Cardinal.lift_eq_one, Field.sepDegree_mul_sepDegree_of_isAlgebraic, Cardinal.sum_const, AddOreLocalization.cardinalMk_le_max, HahnSeries.cardSupp_inv_le, Submodule.FG.spanRank_le_iff_exists_span_set_card_le, card_le_of_injective'', Cardinal.toENat_ne_top, Field.insepDegree_le_of_left_le, Cardinal.aleph0_le_mul_iff, Cardinal.aleph0_lt_continuum, AddMonoidAlgebra.cardinalMk_of_infinite, Cardinal.zero_toNat, Cardinal.succ_pos, LinearMap.le_rank_iff_exists_linearIndependent_finset, Cardinal.card_le_of, LinearMap.rank_finset_sum_le, Cardinal.add_one_le_add_one_iff, Cardinal.card_lt_card_of_right_finite, Cardinal.natCast_le_toENat_iff, Cardinal.lt_ord, Cardinal.out_embedding, Cardinal.lt_aleph0_iff_set_finite, Submodule.LinearDisjoint.rank_inf_le_one_of_flat_right, FirstOrder.Language.card_relations_sum, Cardinal.mk_subset_ge_of_subset_image, Cardinal.mk_punit, continuum_le_cardinal_of_isOpen, Ordinal.cof_iSup_le, FreeAlgebra.cardinalMk_eq_max, Cardinal.mk_unit, Cardinal.aleph_toNat, Cardinal.mk_equiv_eq_zero_iff_lift_ne, Cardinal.natCast_toNat_le, HahnSeries.cardSupp_hsum_le, Cardinal.mk_iUnion_le, Subalgebra.rank_bot, Cardinal.nat_add_aleph0, Subfield.relrank_self, Submodule.LinearDisjoint.rank_inf_le_one_of_flat_left, Cardinal.finset_card_lt_aleph0, rank_matrix'', Cardinal.mk_psum, Module.length_eq_rank, Ordinal.one_le_card, Cardinal.iSup_le_sum, IntermediateField.rank_adjoin_simple_eq_one_iff, Cardinal.add_eq_right_iff, Matrix.rank_vecMulVec, Cardinal.iSup_mk_le_mk_iUnion, rank_subsingleton, Ordinal.le_cof_type, Cardinal.mk_option, Cardinal.toENat_lt_top, Cardinal.succ_aleph0, Cardinal.le_def, ZFSet.iSup_card_le_card_iUnion, Ordinal.card_iSup_le_sum_card, Cardinal.lt_aleph0_iff_fintype, isOpen_setOf_nat_le_rank, Cardinal.mk_finsupp_of_infinite', MvPolynomial.cardinalMk_eq_max_lift, Cardinal.aleph0_le_mk, Cardinal.lift_min, Cardinal.mk_range_le_lift, Cardinal.lift_lt_nat_iff, LinearMap.rank_range_add_rank_ker, Cardinal.add_def, Cardinal.one_le_aleph0, Cardinal.mk_mul_aleph0_eq, HahnSeries.cardSupp_one, FirstOrder.Language.Substructure.lift_card_closure_le, Cardinal.lift_injective, Cardinal.toENat_congr, LinearMap.rank_comp_le_right, FirstOrder.Language.card_le_of_model_distinctConstantsTheory, Cardinal.aleph_zero, Cardinal.toNat_eq_ofNat, Cardinal.one_toNat, Complex.rank_real_complex, Cardinal.continuum_toNat, FreeAlgebra.cardinalMk_eq_max_lift, Cardinal.power_natCast, Cardinal.lift_max, Cardinal.mk_sub_le, Matroid.toENat_cRk_eq, Cardinal.mk_prod, HahnSeries.cardSupp_pow_le, Cardinal.lift_preAleph, Cardinal.lift_lt_aleph_one, Cardinal.toENat_eq_one, LinearMap.lift_rank_comp_le, Cardinal.natCast_le_aleph0, HahnSeries.cardSupp_mul_le, iSupIndep.subtype_ne_bot_le_finrank_aux, Cardinal.aleph0_mul_aleph0, Cardinal.mk_Iio_ord_toType, MvPolynomial.cardinalMk_eq_max, LinearIndependent.cardinalMk_le_finrank, Cardinal.aleph0_add_ofENat, Filter.mem_cardinalGenerate_iff, Cardinal.lift_le, Algebraic.cardinalMk_lift_le_max, FirstOrder.Language.BoundedFormula.card_le, Cardinal.not_isSuccLimit_zero, Cardinal.natCast_mul_lt_natCast_mul, Cardinal.nat_lt_ofENat, Submodule.spanRank_bot, Algebra.rank_adjoin_le, trdeg_le_of_injective, Cardinal.isRegular_preAleph_succ, Polynomial.trdeg_of_isDomain, Cardinal.mk_quaternionAlgebra, FirstOrder.Language.empty.nonempty_embedding_iff
|