mathlib
979f0e83 - feat(data/fin/basic): extract `div_nat` and `mod_nat` from `fin_prod_fin_equiv` (#10339)

Commit
4 years ago
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`.
Author
Parents
Loading