| Name | Category | Theorems |
|---|
aleph0 📖 | CompOp | 237 mathmath: preBeth_omega, ofENat_top, Module.rank_lt_aleph0_iff, add_le_aleph0, Algebra.lift_cardinalMk_adjoin_le, SymmetricAlgebra.rank_eq, Algebraic.cardinalMk_lift_le_mul, mk_list_eq_max_mk_aleph0, IsNoetherian.iff_rank_lt_aleph0, mk_list_le_max, isStrongLimit_aleph0, mk_multiset_of_nonempty, aleph0_add_nat, aleph0_le_continuum, aleph0_mul_ofNat, Computability.Encoding.card_le_aleph0, lift_le_aleph0, mkRat, isPrimePow_iff, range_ofENat, aleph0_le_rank_of_isEmpty_oreSet, sum_pow_le_max_aleph0, nat_mul_aleph0, one_lt_aleph0, ofENat_le_aleph0, aleph0_power_aleph0, le_aleph0_iff_set_countable, ord_aleph0, Matroid.isRkFinite_iff_cRk_lt_aleph0, IsStrongLimit.aleph0_le, mk_le_aleph0_iff, Subfield.cardinalMk_closure_le_max, mul_eq_left_iff, Ordinal.card_omega0, aleph0_le_beth, trdeg_lt_aleph0, Algebraic.cardinalMk_le_max, mk_le_aleph0, nsmul_lt_aleph0_iff_of_ne_zero, Algebra.IsAlgebraic.cardinalMk_le_max, ofENat_lt_aleph0, aleph_mul_aleph0, Ordinal.card_omega0_opow, isInaccessible_def, mk_union_le_aleph0, nat_lt_aleph0, cast_toNat_eq_iff_lt_aleph0, FreeAlgebra.cardinalMk_le_max, preAleph_omega0, ofNat_mul_aleph0, aleph0_add_continuum, toNat_monotoneOn, WType.cardinalMk_le_max_aleph0_of_finite', instCanLiftENatOfENatLeAleph0, strongRankCondition_iff_forall_rank_lt_aleph0, FirstOrder.Language.card_functions_sum_skolem₁_le, add_lt_aleph0_iff, aleph0_le, infinite_iff, IsRegular.aleph0_le, mk_freeMonoid, mk_bounded_set_le, aleph0_le_mk_iff, Submodule.spanRank_finite_iff_fg, hasCardinalLT_aleph0_iff, MeasurableSpace.cardinal_generateMeasurableRec_le, WType.cardinalMk_le_max_aleph0_of_finite, ofNat_le_aleph0, mk_list_eq_max, mk_freeAddGroup, IsInaccessible.aleph0_lt, mk_finsupp_nat, mk_nat, aleph0_le_of_isSuccLimit, beth_zero, lift_eq_aleph0, IntermediateField.cardinalMk_adjoin_le, mk_freeAddMonoid, ofNat_lt_aleph0, power_nat_le_max, aleph0_lt_mk_iff, toNat_strictMonoOn, Algebra.IsAlgebraic.lift_cardinalMk_le_max, continuum_mul_aleph0, Computability.FinEncoding.card_le_aleph0, omega0_le_ord, is_prime_iff, HahnSeries.cardSupp_div_le, Filter.cardinalInterFilter_aleph0, natCast_lt_aleph0, mk_eq_aleph0, CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize, mk_freeRing, Algebraic.cardinalMk_of_countable_of_charZero, aleph0_lt_mk, aleph0_add_ofNat, ord_lt_omega0, aleph0_le_lift, isSuccLimit_aleph0, Ordinal.card_opow_omega0, Ordinal.aleph0_le_card, aleph0_mul_continuum, Set.Countable.le_aleph0, toENat_strictMonoOn, Polynomial.cardinalMk_eq_max, aleph0_add_aleph0, range_aleph, IsAlgClosed.cardinal_le_max_transcendence_basis', Filter.cocardinal_aleph0_eq_cofinite, Matroid.rankInfinite_iff_aleph0_le_cRank, aleph0_le_preAleph, lt_aleph0_iff_subtype_finite, aleph0_le_add_iff, FirstOrder.Language.Term.card_sigma, mk_bounded_subset_le, aleph0_lt_univ, Field.Emb.Cardinal.deg_lt_aleph0, toNat_injOn, mul_lt_aleph0_iff, lt_aleph0_iff_finite, Ordinal.aleph0_le_cof, continuum_add_aleph0, mk_freeGroup, Matroid.rankFinite_iff_cRank_lt_aleph0, cardinal_lt_aleph0_of_finiteDimensional, MeasurableSpace.cardinal_measurableSet_le, MeasurableSpace.cardinal_generateMeasurable_le, aleph0_le_aleph, IsAlgClosed.cardinal_le_max_transcendence_basis, mk_multiset_of_countable, toENat_eq_top, ofENat_add_aleph0, aleph0_lt_aleph_one, LinearIndependent.lt_aleph0_of_finiteDimensional, rank_span_of_finset, continuum_power_aleph0, LinearIndependent.aleph0_le_rank, Algebraic.aleph0_le_cardinalMk_of_charZero, FirstOrder.Language.Term.card_le, ofENat_mul_aleph0, nsmul_lt_aleph0_iff, LinearIndependent.lt_aleph0_of_finite, Algebraic.cardinalMk_le_mul, le_aleph0_iff_subtype_countable, aleph0_le_mul_iff', MvPolynomial.cardinalMk_le_max_lift, toNat_eq_zero, max_aleph0_card_le_rank_fun_nat, FreeAlgebra.cardinalMk_le_max_lift, IntermediateField.lift_cardinalMk_adjoin_le, isSuccPrelimit_aleph0, CategoryTheory.isCardinalFiltered_aleph0_iff, canLiftCardinalNat, aleph0_lt_lift, lift_lt_aleph0, FirstOrder.Language.aleph0_categorical_dlo, lt_aleph0_of_finite, aleph0_eq_lift, denumerable_iff, power_aleph0_of_le_continuum, powerlt_aleph0_le, CategoryTheory.HasCardinalFilteredColimits_iff_hasFilteredColimits, Set.Finite.lt_aleph0, add_eq_left_iff, isRegular_aleph0, aleph0_pos, omega0_lt_ord, lift_aleph0, lt_aleph0, range_natCast, toENat_injOn, two_power_aleph0, Polynomial.cardinalMk_le_max, aleph0_toNat, ofENat_toENat_eq_self, Algebra.cardinalMk_adjoin_le, sum_pow_eq_max_aleph0, aleph0_mul_ofENat, Ordinal.card_lt_aleph0, aleph0_mul_mk_eq, mk_lt_aleph0, mk_lt_aleph0_iff, aleph0_mul_aleph, IsTranscendenceBasis.lift_cardinalMk_eq_max_lift, IsTranscendenceBasis.lift_rank_eq_max_lift, MvRatFunc.rank_eq_max_lift, toNat_pos, MvPolynomial.cardinalMk_le_max, mk_list_eq_aleph0, mk_freeCommRing, mk_freeAbelianGroup, ord_le_omega0, aleph0_mul_nat, HahnSeries.cardSupp_hsum_powers_le, add_le_max, isInaccesible_def, toNat_ne_zero, ofNat_add_aleph0, Ordinal.card_opow_le, ord_eq_omega0, mul_lt_aleph0_iff_of_ne_zero, CategoryTheory.ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable, Module.rank_lt_aleph0, mem_range_aleph_iff, nat_power_aleph0, mul_le_max, HahnSeries.cardSupp_inv_le, Ordinal.cof_omega0, toENat_ne_top, aleph0_le_mul_iff, aleph0_lt_continuum, lt_aleph0_iff_set_finite, FreeAlgebra.cardinalMk_eq_max, mk_pnat, nat_add_aleph0, finset_card_lt_aleph0, fact_isRegular_aleph0, add_eq_right_iff, toENat_lt_top, succ_aleph0, lt_aleph0_iff_fintype, MvPolynomial.cardinalMk_eq_max_lift, aleph0_le_mk, mk_int, one_le_aleph0, mk_mul_aleph0_eq, FirstOrder.Language.Substructure.lift_card_closure_le, aleph_zero, FreeAlgebra.cardinalMk_eq_max_lift, mk_denumerable, natCast_le_aleph0, aleph0_mul_aleph0, MvPolynomial.cardinalMk_eq_max, aleph0_add_ofENat, Algebraic.cardinalMk_lift_le_max, FirstOrder.Language.BoundedFormula.card_le, Algebra.rank_adjoin_le
|
instAdd 📖 | CompOp | 115 mathmath: add_le_aleph0, mk_insert_le, mk_add_one_eq, add_lt_add, aleph0_add_nat, nat_add_continuum, add_one_eq, succ_eq_of_lt_aleph0, succ_natCast, LinearMap.rank_eq_of_surjective, power_add, FirstOrder.Language.card_eq_card_functions_add_card_relations, mk_union_add_mk_inter, Submodule.rank_quotient_add_rank, add_right_inj_of_lt_aleph0, natCast_add_one_le_iff, aleph_add_aleph, add_le_of_le, aleph0_add_continuum, add_eq_self, add_lt_aleph0_iff, sum_nat_eq_add_sum_succ, add_lt_of_lt, trdeg_add_eq, lift_rank_add_lift_rank_le_rank_prod, ofENat_add, LinearMap.lift_rank_eq_of_surjective, rank_quotient_add_rank_of_isDomain, le_mk_diff_add_mk, continuum_add_self, Ordinal.card_add, mk_sum_compl, sum_add_distrib', trdeg_add_le, add_one_le_succ, mk_union_of_disjoint, canonicallyOrderedAdd, add_eq_max', add_nat_le_add_nat_iff, aleph0_add_ofNat, ofNat_add_continuum, add_eq_max, addRightMono, HasRankNullity.rank_quotient_add_rank, aleph0_add_aleph0, add_lt_add_iff_of_left_lt_aleph0, aleph0_le_add_iff, add_eq_left, add_mk_eq_max, ZFSet.card_union_le, LinearMap.lift_rank_range_add_rank_ker, Ordinal.card_succ, Submodule.rank_add_le_rank_add_rank, Submodule.spanRank_sup_le_sum_spanRank, continuum_add_aleph0, rank_quotient_add_rank_le, sum_add_distrib, addLeftMono, ZFSet.card_insert_le, lift_trdeg_add_eq, Matroid.cRk_inter_add_cRk_union_le, Ideal.rank_pow_quot_aux, ZFSet.card_insert, add_one_inj, ofENat_add_aleph0, add_lt_add_iff_of_right_lt_aleph0, continuum_add_ofNat, add_mk_eq_max', mk_sum, continuum_add_nat, HahnSeries.cardSupp_add_le, nat_add_eq, add_nat_inj, add_ciSup, rank_prod', mk_insert, FirstOrder.Language.card_withConstants, add_eq_left_iff, rank_add_rank_le_rank_prod, rank_add_rank_split, ModuleCat.free_shortExact_rank_add, add_one_of_aleph0_le, rank_quotient_add_rank_of_divisionRing, add_nat_eq, FirstOrder.Language.card_functions_sum, LinearMap.rank_add_le, add_mk_eq_self, mk_diff_add_mk, lift_trdeg_add_le, FirstOrder.Language.card_sum, toNat_lift_add_lift, mk_union_le, Submodule.rank_sup_add_rank_inf_eq, ciSup_add_ciSup, lift_add, toNat_add, HahnSeries.cardSupp_sub_le, add_le_max, ofNat_add_aleph0, rank_prod, add_one_le_add_one_iff, FirstOrder.Language.card_relations_sum, add_le_add_iff_of_lt_aleph0, nat_add_aleph0, mk_psum, add_eq_right_iff, mk_option, add_eq_right, ciSup_add, LinearMap.rank_range_add_rank_ker, add_def, FirstOrder.Language.Substructure.lift_card_closure_le, add_lt_aleph0, aleph0_add_ofENat, FirstOrder.Language.BoundedFormula.card_le
|
instInhabited 📖 | CompOp | — |
instMul 📖 | CompOp | 134 mathmath: continuum_mul_ofNat, mk_sUnion_le, Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic, lift_rank_mul_lift_rank, Algebraic.cardinalMk_lift_le_mul, aleph0_mul_ofNat, mul_aleph0_eq, power_mul, rank_finsupp, Field.insepDegree_mul_insepDegree_of_isAlgebraic, mul_le_max_of_aleph0_le_right, nat_mul_aleph0, natCast_mul_inj, toNat_mul, mul_eq_max_of_aleph0_le_right, sum_le_mk_mul_iSup, IntermediateField.relrank_mul_rank_top, Subalgebra.rank_sup_eq_rank_left_mul_rank_of_free, mul_eq_left_iff, mul_natCast_le_mul_natCast, power_add, mul_eq_left, rank_matrix_module, Subfield.relrank_mul_rank_top, continuum_mul_self, rank_mul_rank, mk_div_le, IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic, aleph_mul_aleph0, Field.rank_mul_sepDegree_of_isSeparable, mk_setProd, mul_natCast_strictMono, mk_biUnion_le_lift, ofNat_mul_aleph0, Subalgebra.LinearDisjoint.rank_sup_of_free, nat_mul_continuum, Module.rank_linearMap, IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right, continuum_mul_nat, mul_eq_max, mul_eq_self, ofNat_mul_continuum, Ordinal.card_iSup_Iio_le_card_mul_iSup, mul_def, mul_ciSup, mk_image2_le, Field.rank_mul_insepDegree_of_isPurelyInseparable, ciSup_mul, Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, rank_tensorProduct, mul_le_max_of_aleph0_le_left, continuum_mul_aleph0, ofENat_mul, HahnSeries.cardSupp_div_le, sum_le_lift_mk_mul_iSup, mul_natCast_inj, mul_mk_eq_max, Subfield.relrank_mul_relrank_eq_inf_relrank, le_mul_left, aleph0_mul_eq, 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, aleph0_mul_continuum, sum_const', mk_biUnion_le, Subalgebra.rank_sup_eq_rank_right_mul_rank_of_free, mul_eq_right, mul_lt_of_lt, Subfield.relrank_inf_mul_relrank_of_le, rank_matrix_module', sum_le_iSup_lift, mk_iUnion_le_lift, natCast_mul_strictMono, le_mul_right, IntermediateField.LinearDisjoint.rank_sup, IntermediateField.rank_sup_le_of_isAlgebraic, rank_matrix', mul_lt_aleph0_iff, Field.sepDegree_mul_insepDegree, rank_matrix, sum_le_lift_mk_mul_iSup_lift, IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left, mk_mul_le, IntermediateField.relrank_inf_mul_relrank_of_le, Subalgebra.rank_sup_le_of_free, aleph_mul_aleph, Ordinal.card_mul, noZeroDivisors, ofENat_mul_aleph0, mul_power, IntermediateField.relrank_mul_relrank, Algebraic.cardinalMk_le_mul, aleph0_le_mul_iff', mul_lt_aleph0, IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left, ciSup_mul_ciSup, IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, rank_real_of_complex, lift_mul, mk_add_le, natCast_mul_le_natCast_mul, IntermediateField.rank_sup_le, mul_eq_max_of_aleph0_le_left, mul_natCast_lt_mul_natCast, rank_finsupp', Field.lift_rank_mul_lift_sepDegree_of_isSeparable, sum_le_iSup, rank_fun, aleph0_mul_ofENat, lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le, aleph0_mul_mk_eq, IntermediateField.rank_bot_mul_relrank, Subfield.relrank_mul_relrank, aleph0_mul_aleph, rank_fun_eq_lift_mul, IntermediateField.relrank_inf_mul_relrank, aleph0_mul_nat, mul_lt_aleph0_iff_of_ne_zero, rank_tensorProduct', IntermediateField.relrank_mul_relrank_eq_inf_relrank, mul_le_max, Field.sepDegree_mul_sepDegree_of_isAlgebraic, sum_const, mk_le_mk_mul_of_mk_preimage_le, aleph0_le_mul_iff, mk_iUnion_le, rank_matrix'', mk_mul_aleph0_eq, mk_sub_le, mk_prod, HahnSeries.cardSupp_mul_le, aleph0_mul_aleph0, natCast_mul_lt_natCast_mul
|
instNatCast 📖 | CompOp | 197 mathmath: natCast_lt_toENat_iff, Submodule.fg_iff_spanRank_eq_spanFinrank, natCast_le_rank_iff_finset, toENat_eq_natCast_iff, linearIndependent_le_span, linearIndependent_le_span_finset, ofENat_ofNat, two_le_iff_one_lt, Quaternion.rank_eq_four, aleph0_add_nat, toNat_eq_iff, ofNat_le_lift_iff, linearIndependent_le_span', nat_add_continuum, isPrimePow_iff, exists_spanRank_le_and_le_height_of_le_height, nat_mul_aleph0, natCast_mul_inj, card_le_of_finset, rank_eq_card_basis, mk_fin, Module.le_rank_iff_exists_linearMap, succ_natCast, ofNat_lt_lift_iff, mk_eq_nat_iff, mul_natCast_le_mul_natCast, FixedPoints.rank_le_card, algebraicIndependent_bounded_of_finset_algebraicIndependent_bounded, toENat_eq_ofNat, IsStrongLimit.two_power_lt, lift_lt_ofNat_iff, preAleph_nat, LinearMap.rank_diagonal, mk_eq_two_iff', Nat.count_le_cardinal, Field.Emb.Cardinal.two_le_deg, FirstOrder.Language.Sentence.realize_cardGe, MvPolynomial.rank_R, Matrix.cRank_le_card_height, toENatAux_eq_nat, mk_le_iff_forall_finset_subset_card_le, toENat_lt_natCast_iff, natCast_le_rank_iff, nat_lt_aleph0, natCast_add_one_le_iff, mul_natCast_strictMono, cast_toNat_eq_iff_lt_aleph0, toENatAux_nat, nat_lt_continuum, Algebra.IsStandardSmoothOfRelativeDimension.iff_of_isStandardSmooth, nat_eq_ofENat, beth_succ, Ordinal.nat_le_card, lift_le_nat_iff, toENat_le_ofNat, nat_mul_continuum, Module.le_rank_iff, aleph0_le, LinearRecurrence.solSpace_rank, Module.finrank_eq_card_basis', RCLike.rank_le_two, continuum_mul_nat, nat_coe_dvd_iff, IsInaccessible.nat_lt, Ordinal.nat_lt_card, Module.le_rank_iff_exists_finset, Matrix.cRank_le_card_width, MeasurableSpace.cardinal_generateMeasurableRec_le, mk_coe_finset, QuadraticAlgebra.rank_eq_two, IsClosed.two_pow_mk_le_two_pow_mk_dense, power_self_eq, Ordinal.card_lt_nat, Module.lt_rank_of_lt_finrank, ZFSet.card_pair_of_ne, lift_mk_fin, lift_le_ofNat_iff, Ordinal.card_ofNat, mk_perm_eq_two_power, mk_equiv_of_eq, nat_eq_lift_iff, toNat_rightInverse, power_nat_le_max, QuaternionAlgebra.rank_eq_four, linearIndependent_bounded_of_finset_linearIndependent_bounded, Complex.rank_real_complex', is_prime_iff, rank_span_finset_le, mk_powerset, natCast_lt_aleph0, mk_fintype, mul_natCast_inj, add_nat_le_add_nat_iff, nat_power_eq, lift_eq_ofNat_iff, Module.finrank_eq_rank, ofENat_eq_nat, Submodule.IsLattice.rank_of_pi, Submodule.finrank_eq_rank, nat_lt_lift_iff, IsClosed.two_pow_mk_lt_continuum, Ordinal.card_le_nat, not_isSuccLimit_natCast, lift_two, cantor, cast_toNat_of_aleph0_le, preBeth_succ, nat_succ, lift_natCast, Nat.cast_card, Module.mk_finrank_eq_card_basis, mk_bool, ord_nat, natCast_mul_strictMono, mk_eq_two_iff, mk_finset_of_fintype, mk_eq_nat_iff_finset, ofENat_nat, mk_eq_nat_iff_fintype, MeasurableSpace.cardinal_measurableSet_le, lift_two_power, two_le_iff, MeasurableSpace.cardinal_generateMeasurable_le, one_lt_two, Ordinal.card_eq_nat, mk_set, two_le_iff', Module.rank_eq_ofNat_iff_finrank_eq_ofNat, Set.cast_ncard, ofENat_lt_nat, nat_is_prime_iff, mk_Prop, rank_fin_fun, lift_ofNat, toENat_le_natCast_iff, toENatAux_le_nat, toENat_le_nat, Field.Emb.cardinal_eq_two_pow_sepDegree, cast_toNat_of_lt_aleph0, rank_real_of_complex, continuum_add_nat, Module.finrank_eq_rank', nat_add_eq, Ordinal.card_nat, canLiftCardinalNat, natCast_mul_le_natCast_mul, add_nat_inj, mk_set_eq_nat_iff_finset, lt_aleph0, Algebra.SubmersivePresentation.rank_kaehlerDifferential, range_natCast, toENat_eq_nat, two_power_aleph0, basis_le_span', mul_natCast_lt_mul_natCast, ofNat_eq_lift_iff, ZFSet.card_powerset, nat_le_ofENat, toNat_natCast, add_nat_eq, rank_fun, IsRegular.nat_lt, toNat_apply_of_lt_aleph0, cardinalMk_algHom, rank_fun', nat_le_lift_iff, le_rank_iff_exists_linearIndependent_finset, IsClosed.mk_lt_two_pow_mk_dense, rank_fun_eq_lift_mul, natCast_eq_toENat_iff, ofENat_le_nat, Algebra.IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential, aleph0_mul_nat, toENat_nat, lift_eq_nat_iff, preBeth_nat, mk_equiv_of_lift_eq, FirstOrder.Ring.card_ring, rank_le, nat_power_aleph0, nat_lt_univ, Field.Emb.cardinal_eq_two_pow_rank, LinearMap.le_rank_iff_exists_linearIndependent_finset, card_le_of, natCast_le_toENat_iff, natCast_toNat_le, nat_add_aleph0, isOpen_setOf_nat_le_rank, lift_lt_nat_iff, toNat_eq_ofNat, Complex.rank_real_complex, power_natCast, natCast_le_aleph0, iSupIndep.subtype_ne_bot_le_finrank_aux, LinearIndependent.cardinalMk_le_finrank, natCast_mul_lt_natCast_mul, nat_lt_ofENat
|
instOne 📖 | CompOp | 141 mathmath: mk_insert_le, mk_add_one_eq, HahnSeries.cardSupp_single_of_ne, two_le_iff_one_lt, rank_le_one, one_eq_ofENat, sum_zero_pow, Matrix.cRank_subsingleton, one_lt_aleph0, HahnSeries.cardSupp_single_le, Ordinal.card_one, IntermediateField.relrank_eq_one_iff, add_one_eq, succ_eq_of_lt_aleph0, rank_eq_one, succ_natCast, ZFSet.card_singleton, mk_le_one_iff_set_subsingleton, mul_eq_left_iff, Ordinal.cof_eq_one_iff_is_succ, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat, Field.sepDegree_self, Subfield.relrank_eq_one_of_le, Module.one_lt_rank_of_one_lt_finrank, Subfield.relrank_top_left, IsPurelyInseparable.sepDegree_eq_one, rank_submodule_le_one_iff, Module.one_le_rank_iff, CommSemiring.rank_self, le_one_iff_subsingleton, zero_power_le, HahnSeries.cardSupp_one_le, preBeth_one, natCast_add_one_le_iff, Submodule.LinearDisjoint.rank_inf_le_one_of_flat, LinearEquiv.mem_dilatransvections_iff_rank, Ordinal.card_le_one, lt_one_iff_zero, ModularForm.levelOne_weight_zero_rank_one, one_le_ofENat, ord_eq_one, one_le_iff_ne_zero, InnerProductSpace.rank_rankOne, FirstOrder.Language.order.card_eq_one, IntermediateField.rank_adjoin_eq_one_iff, rank_submodule_le_one_iff', IntermediateField.rank_top, Ordinal.one_lt_card, one_power, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_right, Ordinal.cof_succ, Set.Subsingleton.cardinalMk_le_one, IntermediateField.relrank_top_left, MvPolynomial.cardinalMk_eq_one, ofENat_eq_one, rank_eq_one_iff, add_one_le_succ, mk_set_eq_one_iff, IntermediateField.sepDegree_bot, isUnit_iff, Module.Invertible.rank_eq_one, toNat_eq_one, IntermediateField.rank_bot, Subalgebra.LinearDisjoint.rank_eq_one_of_commute_of_flat_of_self_of_inj, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_of_inj, eq_one_iff_unique, power_one, rank_submodule_eq_one_iff, power_zero, collinear_iff_rank_le_one, lift_le_one_iff, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_left_of_inj, IntermediateField.relrank_eq_one_of_le, Ordinal.card_succ, ord_one, Module.rank_self, IntermediateField.rank_eq_one_iff, Field.insepDegree_self, Submodule.LinearDisjoint.rank_le_one_of_flat_of_self, ZFSet.card_insert_le, one_lt_two, Ordinal.card_eq_one, ZFSet.card_insert, add_one_inj, one_lt_iff_nontrivial, one_lt_ofENat, Submodule.LinearDisjoint.rank_le_one_of_commute_of_flat_of_self, Module.rank_le_one_iff_top_isPrincipal, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_of_inj, one_lt_lift_iff, ofENat_le_one, Algebra.IsSeparable.insepDegree_eq, Module.rank_eq_one_iff_finrank_eq_one, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj, one_eq_lift_iff, IntermediateField.relrank_self, Subalgebra.rank_eq_one_iff, mk_insert, Submodule.rank_le_one_iff_isPrincipal, Subfield.relrank_eq_one_iff, IntermediateField.relrank_bot_right, succ_zero, lift_one, toENat_le_one, zero_powerlt, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_left_of_inj, mk_singleton, trdeg_subsingleton, add_one_of_aleph0_le, mk_multiset_of_isEmpty, mk_eq_one, one_le_lift_iff, IntermediateField.insepDegree_bot, rank_le_one_iff, FreeAlgebra.cardinalMk_eq_one, one_le_iff_pos, Submodule.LinearDisjoint.rank_inf_le_one_of_commute_of_flat_left, Subalgebra.LinearDisjoint.rank_inf_eq_one_of_commute_of_flat_right_of_inj, mk_plift_true, power_le_max_power_one, Subalgebra.bot_eq_top_iff_rank_eq_one, ofENat_one, Subalgebra.LinearDisjoint.rank_eq_one_of_flat_of_self_of_inj, lift_eq_one, add_one_le_add_one_iff, Submodule.LinearDisjoint.rank_inf_le_one_of_flat_right, mk_punit, mk_unit, Subalgebra.rank_bot, Subfield.relrank_self, Submodule.LinearDisjoint.rank_inf_le_one_of_flat_left, Ordinal.one_le_card, IntermediateField.rank_adjoin_simple_eq_one_iff, Matrix.rank_vecMulVec, rank_subsingleton, mk_option, one_le_aleph0, HahnSeries.cardSupp_one, one_toNat, toENat_eq_one, Polynomial.trdeg_of_isDomain
|
instPowCardinal 📖 | CompOp | 68 mathmath: self_le_power, power_mul, power_le_power_right, aleph0_power_aleph0, pow_eq, prod_eq_two_power, power_add, IsStrongLimit.two_power_lt, prod_const, lt_power_cof, zero_power_le, pow_le, beth_succ, WType.cardinalMk_eq_sum_lift, lift_power_sum, mk_bounded_set_le, lt_cof_power, MeasurableSpace.cardinal_generateMeasurableRec_le, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank, IsClosed.two_pow_mk_le_two_pow_mk_dense, power_self_eq, one_power, mk_perm_eq_two_power, prod_const', mk_equiv_of_eq, power_nat_le_max, cardinalMk_eq_cardinalMk_field_pow_rank, le_powerlt, mk_powerset, nat_power_eq, powerlt_le, power_one, IsClosed.two_pow_mk_lt_continuum, cantor, WType.cardinalMk_eq_sum, power_zero, mk_arrow, mk_bounded_subset_le, preBeth_succ, MeasurableSpace.cardinal_measurableSet_le, lift_two_power, MeasurableSpace.cardinal_generateMeasurable_le, mk_perm_eq_self_power, mk_set, continuum_power_aleph0, zero_power, mul_power, power_sum, Field.Emb.cardinal_eq_two_pow_sepDegree, powerlt_succ, power_aleph0_of_le_continuum, power_pos, mk_bounded_set_le_of_infinite, two_power_aleph0, ZFSet.card_powerset, IsClosed.mk_lt_two_pow_mk_dense, cantor', lift_power, power_le_power_left, power_lt_aleph0, power_le_max_power_one, mk_equiv_of_lift_eq, power_def, nat_power_aleph0, Field.Emb.cardinal_eq_two_pow_rank, power_le_aleph0, power_natCast, power_eq_two_power
|
instZero 📖 | CompOp | 100 mathmath: mk_eq_zero, mk_emptyCollection_iff, trdeg_eq_zero_of_not_injective, preBeth_eq_zero, aleph_pos, Ordinal.cof_zero, iSup_of_empty, sum_zero_pow, rank_zero_iff_forall_zero, lift_zero, Ordinal.card_zero, toENat_eq_zero, mul_eq_left_iff, rank_bot, ModularForm.levelOne_neg_weight_rank_zero, trdeg_eq_zero, zero_le, mk_emptyCollection, Module.rank_pos_iff_of_free, ord_eq_zero, rank_subsingleton', Field.instNeZeroInsepDegree, zero_power_le, mk_embedding_eq_zero_iff_lift_lt, lt_one_iff_zero, Ordinal.card_eq_zero, prod_eq_zero, rank_pos_iff_nontrivial, univ_pos, ofENat_eq_zero, preBeth_zero, Module.rank_pos_of_free, powerlt_zero, zero_eq_lift_iff, ord_zero, rank_eq_zero_iff_isTorsion, continuum_pos, mk_equiv_eq_zero_iff_ne, IsInaccessible.pos, mk_eq_zero_iff, sInf_eq_zero_iff, Submodule.rank_eq_zero, rank_punit, beth_pos, HahnSeries.cardSupp_zero, Module.rank_zero_iff_of_free, power_zero, cast_toNat_of_aleph0_le, trdeg_pos, FirstOrder.Language.card_empty, mul_lt_aleph0_iff, preAleph_zero, LinearMap.rank_zero, sInf_empty, not_isStrongLimit_zero, toENatAux_zero, Field.instNeZeroSepDegree, Ordinal.zero_lt_card, mk_surjective_eq_zero_iff, toENatAux_eq_zero, zero_power, ofENat_pos, noZeroDivisors, Matrix.cRank_zero, mk_plift_false, toNat_eq_zero, rank_pos_iff_exists_ne_zero, mk_pempty, preAleph_pos, add_eq_left_iff, aleph0_pos, isSuccPrelimit_zero, mk_set_eq_zero_iff, succ_zero, zero_powerlt, zero_eq_ofENat, rank_eq_zero_iff, ZFSet.card_empty, Submodule.spanRank_eq_zero_iff_eq_bot, rank_pos, mk_surjective_eq_zero_iff_lift, iInf_eq_zero_iff, rank_zero_iff, Ordinal.cof_eq_zero, mk_arrow_eq_zero_iff, one_le_iff_pos, IsRegular.pos, mk_empty, preBeth_pos, lift_eq_zero, ofENat_zero, trdeg_eq_zero_iff, mk_embedding_eq_zero_iff_lt, zero_lt_lift_iff, zero_toNat, succ_pos, mk_equiv_eq_zero_iff_lift_ne, add_eq_right_iff, not_isSuccLimit_zero, Submodule.spanRank_bot
|
isEquivalent 📖 | CompOp | 4 mathmath: mk_out, nonempty_out, out_lift_equiv, out_embedding
|
map 📖 | CompOp | 1 mathmath: map_mk
|
map₂ 📖 | CompOp | — |
mk 📖 | CompOp | — |
outMkEquiv 📖 | CompOp | — |
prod 📖 | CompOp | 11 mathmath: mk_pi, prod_eq_two_power, lift_prod, prod_const, lift_power_sum, prod_eq_zero, prod_const', prod_eq_of_fintype, sum_lt_prod, power_sum, prod_le_prod
|
sum 📖 | CompOp | 46 mathmath: Ordinal.lift_card_iSup_le_sum_card, sum_lt_of_isRegular, le_sum, sum_zero_pow, sum_pow_le_max_aleph0, Ordinal.card_iSup_Iio_le_sum_card, mk_list_eq_sum_pow, sum_le_mk_mul_iSup, rank_directSum, sum_eq_lift_iSup_of_lift_mk_le_lift_iSup, FirstOrder.Language.card_eq_card_functions_add_card_relations, mk_iUnion_le_sum_mk_lift, mk_iUnion_eq_sum_mk, sum_lt_lift_of_isRegular, WType.cardinalMk_eq_sum_lift, lift_power_sum, mk_iUnion_le_sum_mk, sum_eq_iSup, TensorAlgebra.rank_eq, lift_sum, sum_nat_eq_add_sum_succ, sum_eq_iSup_of_mk_le_iSup, mk_iUnion_eq_sum_mk_lift, sum_le_sum, sum_add_distrib', lift_iSup_le_sum, ZFSet.lift_card_iUnion_le_sum_card, sum_le_lift_mk_mul_iSup, WType.cardinalMk_eq_sum, sum_const', sum_le_iSup_lift, sum_add_distrib, sum_le_lift_mk_mul_iSup_lift, sum_eq_iSup_lift, sum_lt_prod, lift_le_sum, power_sum, mk_sigma, sum_le_iSup, sum_pow_eq_max_aleph0, sum_const, rank_pi, HahnSeries.cardSupp_hsum_le, iSup_le_sum, Ordinal.card_iSup_le_sum_card, sum_eq_iSup_of_lift_mk_le_iSup
|
termℵ₀ 📖 | CompOp | — |
«term#_» 📖 | CompOp | — |