mathlib
404520a1 - feat(group_theory/index): `nat.card` version of `card_dvd_of_le` (#17269)

Commit

3 years ago

feat(group_theory/index): `nat.card` version of `card_dvd_of_le` (#17269) This PR adds a `nat.card` version of `card_dvd_of_le`.

Author

tb65536

Parents