Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-07-12 12:15 3a2b5524

View on Github →

feat(data/fin/basic): extra instances that cover fin 0 (#18970) These apply to fin 0, unlike the comm_ring instance which needs ne_zero n.

Estimated changes