Cardinality

📁 Source: Mathlib/RingTheory/Algebraic/Cardinality.lean

Statistics

Metric	Count
Definitions	0
Theorems cardinalMk_le_max, cardinalMk_le_sigma_polynomial, lift_cardinalMk_le_max, lift_cardinalMk_le_sigma_polynomial	4
Total	4

Algebra.IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_le_max 📖	mathematical	—	Cardinal Cardinal.instLE SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	Cardinal.lift_id lift_cardinalMk_le_max
cardinalMk_le_sigma_polynomial 📖	mathematical	—	Cardinal Cardinal.instLE Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Multiset Multiset.instMembership Polynomial.aroots	—	Cardinal.lift_id lift_cardinalMk_le_sigma_polynomial
lift_cardinalMk_le_max 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	lift_cardinalMk_le_sigma_polynomial Cardinal.mk_sigma Cardinal.sum_le_sum LT.lt.le Set.Finite.lt_aleph0 Multiset.finite_toSet Cardinal.sum_const Cardinal.lift_aleph0 LE.le.trans Cardinal.mul_le_max sup_le_sup le_refl Cardinal.lift_max sup_of_le_left
lift_cardinalMk_le_sigma_polynomial 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Multiset Multiset.instMembership Polynomial.aroots	—	Cardinal.lift_mk_le_lift_mk_of_injective isAlgebraic Polynomial.map_ne_zero_iff FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial Polynomial.mem_roots Polynomial.IsRoot.eq_1 Polynomial.eval_map Polynomial.aeval_def Subtype.heq_iff_coe_eq Polynomial.aroots.congr_simp Cardinal.lift_id' Cardinal.lift_umax

---

← Back to Index