Cardinal

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

Statistics

Metric	Count
Definitions	0
Theorems cardinalMk_lift_of_fintype, cardinalMk_lift_of_infinite, cardinalMk_lift_of_infinite', cardinalMk_of_fintype, cardinalMk_of_infinite, cardinalMk_of_infinite', cardinalMk_lift_of_fintype, cardinalMk_lift_of_infinite, cardinalMk_lift_of_infinite', cardinalMk_of_fintype, cardinalMk_of_infinite, cardinalMk_of_infinite'	12
Total	12

AddMonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_lift_of_fintype 📖	mathematical	—	AddMonoidAlgebra Cardinal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Cardinal.commSemiring Cardinal.lift Fintype.card	—	Cardinal.mk_finsupp_lift_of_fintype
cardinalMk_lift_of_infinite 📖	mathematical	—	AddMonoidAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift	—	Cardinal.mk_finsupp_lift_of_infinite max_comm
cardinalMk_lift_of_infinite' 📖	mathematical	—	AddMonoidAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift	—	Cardinal.mk_finsupp_lift_of_infinite' max_comm
cardinalMk_of_fintype 📖	mathematical	—	AddMonoidAlgebra Cardinal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Cardinal.commSemiring Fintype.card	—	cardinalMk_lift_of_fintype Cardinal.lift_id
cardinalMk_of_infinite 📖	mathematical	—	AddMonoidAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot	—	cardinalMk_lift_of_infinite Cardinal.lift_id
cardinalMk_of_infinite' 📖	mathematical	—	AddMonoidAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot	—	cardinalMk_lift_of_infinite' Cardinal.lift_id

MonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_lift_of_fintype 📖	mathematical	—	MonoidAlgebra Cardinal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Cardinal.commSemiring Cardinal.lift Fintype.card	—	Cardinal.mk_finsupp_lift_of_fintype
cardinalMk_lift_of_infinite 📖	mathematical	—	MonoidAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift	—	Cardinal.mk_finsupp_lift_of_infinite max_comm
cardinalMk_lift_of_infinite' 📖	mathematical	—	MonoidAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot Cardinal.lift	—	Cardinal.mk_finsupp_lift_of_infinite' max_comm
cardinalMk_of_fintype 📖	mathematical	—	MonoidAlgebra Cardinal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Cardinal.commSemiring Fintype.card	—	cardinalMk_lift_of_fintype Cardinal.lift_id
cardinalMk_of_infinite 📖	mathematical	—	MonoidAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot	—	cardinalMk_lift_of_infinite Cardinal.lift_id
cardinalMk_of_infinite' 📖	mathematical	—	MonoidAlgebra Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Cardinal.instConditionallyCompleteLinearOrderBot	—	cardinalMk_lift_of_infinite' Cardinal.lift_id

---

← Back to Index