fincard): Define `nat`- and `enat`-valued cardinalities (#6494)

Commit

4 years ago

feat(set_theory/cardinal, data/nat/fincard): Define `nat`- and `enat`-valued cardinalities (#6494) Defines `cardinal.to_nat` and `cardinal.to_enat` Uses those to define `nat.card` and `enat.card`

Author

awainverse

Parents

9607dbdd

mathlib3 1cc59b9d - feat(set_theory/cardinal, data/nat/fincard): Define `nat`- and `enat`-valued cardinalities (#6494)

mathlib3
1cc59b9d - feat(set_theory/cardinal, data/nat/fincard): Define `nat`- and `enat`-valued cardinalities (#6494)