Mathlib v3 is deprecated. Go to Mathlib v4

Def fin.mod_nat

Modification history

2021-11-16 04:55
src/data/fin/basic.lean
feat(data/fin/basic): extract `div_nat` and `mod_nat` from `fin_prod_fin_equiv` (#10339) …
Added fin.mod_natView on Github →