mathlib3

464d04af - feat(data/nat/fincard): introduce `nat.card`, `enat.card` (#6670)

feat(data/nat/fincard): introduce `nat.card`, `enat.card` (#6670) Defines `nat`- and `enat`-valued cardinality functions. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>