*): move `nat.infinite` to `fintype.card` (#17745)

Commit

3 years ago

chore(data/fintype/*): move `nat.infinite` to `fintype.card` (#17745) Also import `fintype.card` instead of `fintype.lattice` in `algebra.char_zero.infinite`.

Author

urkud

Parents

5a61ec7d

mathlib eb1f1ac6 - chore(data/fintype/*): move `nat.infinite` to `fintype.card` (#17745)

mathlib
eb1f1ac6 - chore(data/fintype/*): move `nat.infinite` to `fintype.card` (#17745)