Cardinal

📁 Source: Mathlib/Algebra/MvPolynomial/Cardinal.lean

Statistics

Metric	Count
Definitions	0
Theorems cardinalMk_eq, cardinalMk_eq_lift, cardinalMk_eq_max, cardinalMk_eq_max_lift, cardinalMk_eq_one, cardinalMk_le_max, cardinalMk_le_max_lift	7
Total	7

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_eq 📖	mathematical	—	MvPolynomial	—	cardinalMk_eq_lift Cardinal.lift_id
cardinalMk_eq_lift 📖	mathematical	—	MvPolynomial Cardinal.lift	—	AddMonoidAlgebra.cardinalMk_eq_lift_of_fintype Fintype.card_unique pow_one
cardinalMk_eq_max 📖	mathematical	—	MvPolynomial Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	cardinalMk_eq_max_lift Cardinal.lift_id sup_assoc
cardinalMk_eq_max_lift 📖	mathematical	—	MvPolynomial Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Cardinal.aleph0	—	AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite Finsupp.infinite_of_right instInfiniteNat Cardinal.mk_finsupp_lift_of_infinite' Cardinal.lift_uzero Cardinal.mk_eq_aleph0 instCountableNat Cardinal.lift_aleph0 Cardinal.lift_max sup_assoc
cardinalMk_eq_one 📖	mathematical	—	MvPolynomial Cardinal Cardinal.instOne	—	Cardinal.mk_eq_one Unique.instSubsingleton
cardinalMk_le_max 📖	mathematical	—	Cardinal Cardinal.instLE MvPolynomial SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.aleph0	—	LE.le.trans cardinalMk_le_max_lift Cardinal.lift_id le_refl
cardinalMk_le_max_lift 📖	mathematical	—	Cardinal Cardinal.instLE MvPolynomial SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift Cardinal.aleph0	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Cardinal.mk_fintype Fintype.card_unique Nat.cast_one isEmpty_or_nonempty cardinalMk_eq_lift Cardinal.mk_eq_zero Cardinal.lift_zero sup_of_le_left Cardinal.canonicallyOrderedAdd cardinalMk_eq_max_lift instReflLe

---

← Back to Index