Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-16 04:55 979f0e83

View on Github →

feat(data/fin/basic): extract div_nat and mod_nat from fin_prod_fin_equiv (#10339) This makes it a little easier to tell which component is div and which is mod from the docs alone, and also makes these available earlier than data/equiv/fin.

Estimated changes