AlgebraicCard

📁 Source: Mathlib/Algebra/AlgebraicCard.lean

Statistics

Metric	Count
Definitions	0
Theorems aleph0_le_cardinalMk_of_charZero, cardinalMk_le_max, cardinalMk_le_mul, cardinalMk_lift_le_max, cardinalMk_lift_le_mul, cardinalMk_lift_of_infinite, cardinalMk_of_countable_of_charZero, cardinalMk_of_infinite, countable, infinite_of_charZero	10
Total	10

Algebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aleph0_le_cardinalMk_of_charZero 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.aleph0 IsAlgebraic	—	Cardinal.infinite_iff Set.infinite_coe_iff infinite_of_charZero
cardinalMk_le_max 📖	mathematical	—	Cardinal Cardinal.instLE IsAlgebraic CommRing.toRing SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	Cardinal.lift_id cardinalMk_lift_le_max
cardinalMk_le_mul 📖	mathematical	—	Cardinal Cardinal.instLE IsAlgebraic CommRing.toRing Cardinal.instMul Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Cardinal.aleph0	—	Cardinal.lift_id cardinalMk_lift_le_mul
cardinalMk_lift_le_max 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift IsAlgebraic CommRing.toRing SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	LE.le.trans cardinalMk_lift_le_mul le_imp_le_of_le_of_le mul_le_mul_left covariant_swap_mul_of_covariant_mul CanonicallyOrderedAdd.toMulLeftMono Cardinal.canonicallyOrderedAdd Cardinal.lift_le Polynomial.cardinalMk_le_max le_refl Cardinal.lift_max Cardinal.lift_aleph0 Cardinal.mul_aleph0_eq
cardinalMk_lift_le_mul 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift IsAlgebraic CommRing.toRing Cardinal.instMul Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Cardinal.aleph0	—	Cardinal.mk_uLift Cardinal.lift_mk_le_lift_mk_mul_of_lift_mk_preimage_le Cardinal.lift_le_aleph0 Cardinal.le_aleph0_iff_set_countable Polynomial.mem_rootSet Set.MapsTo.countable_of_injOn Function.Injective.injOn Subtype.coe_injective Set.Finite.countable Polynomial.rootSet_finite Subtype.coe_prop
cardinalMk_lift_of_infinite 📖	mathematical	—	Cardinal.lift IsAlgebraic CommRing.toRing	—	LE.le.antisymm LE.le.trans_eq cardinalMk_lift_le_max max_eq_left instInfiniteULift Cardinal.lift_mk_le' isAlgebraic_algebraMap IsDomain.toNontrivial FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero
cardinalMk_of_countable_of_charZero 📖	mathematical	—	IsAlgebraic CommRing.toRing Cardinal.aleph0	—	LE.le.antisymm Set.Countable.le_aleph0 countable aleph0_le_cardinalMk_of_charZero
cardinalMk_of_infinite 📖	mathematical	—	IsAlgebraic CommRing.toRing	—	cardinalMk_lift_of_infinite
countable 📖	mathematical	—	Set.Countable setOf IsAlgebraic CommRing.toRing	—	Cardinal.le_aleph0_iff_set_countable Cardinal.lift_le_aleph0 LE.le.trans cardinalMk_lift_le_max sup_of_le_right
infinite_of_charZero 📖	mathematical	—	Set.Infinite setOf IsAlgebraic	—	Set.infinite_of_injective_forall_mem instInfiniteNat Nat.cast_injective isAlgebraic_nat MulActionWithZero.nontrivial instNontrivialOfCharZero

---

← Back to Index