Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-12 11:00 008af8bb

View on Github →

chore(data/fin/basic): remove fin.coe_of_nat_eq_mod (#18131) It can be proved by fin.coe_of_nat_eq_mod'.

Estimated changes

deleted theorem fin.coe_of_nat_eq_mod'
modified theorem fin.coe_of_nat_eq_mod