finite): Add `nat.card_fun` (#16799)

Commit

3 years ago

feat(set_theory/cardinal/finite): Add `nat.card_fun` (#16799) This PR adds `nat.card_fun`, a quick consequence of `nat.card_pi`.

Author

tb65536

Parents