Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-14 03:22 464d04af

View on Github →

feat(data/nat/fincard): introduce nat.card, enat.card (#6670) Defines nat- and enat-valued cardinality functions.

Estimated changes

added def enat.card
added def nat.card