mathlib

3a2b5524 - feat(data/fin/basic): extra instances that cover `fin 0` (#18970)

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`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>