Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-20 18:58 404520a1

View on Github →

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.

Estimated changes