Cardinality

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinalMk` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisorsLeft` `Semiring.toMonoidWithZero`	`OreLocalization` `MonoidWithZero.toMonoid` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Semiring.toModule`	—	`le_antisymm` `cardinalMk_le` `Cardinal.mk_le_of_injective`

---