ENat.card, Nat.card

Stream: mathlib4

[Yury G. Kudryashov]

Hi, I finally started working on adding ENat.card and redefining Nat.card the way I want to see it in Mathlib.

[Yury G. Kudryashov]

Tracking issue is #9794, comments are welcome.

[Yury G. Kudryashov]

The first PR is #9792. It lacks documentation, otherwise should be is ready for review.

[Yury G. Kudryashov]

As for ENat.card and Nat.card, I'm going to port some code from my old mathlib3 branch

[Floris van Doorn]

This looks good to me. Is "Define ENat.card without using Cardinals" just to avoid the dependency?

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

Then we can redefine Cardinal.toENat as Quotient.lift ENat.card _