mathlib3

eaeb4583 - feat(set_theory/cardinal/finite): `nat.card (zmod n) = n` (#16118)

feat(set_theory/cardinal/finite): `nat.card (zmod n) = n` (#16118) This PR adds a short lemma `nat.card (zmod n) = n`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>