mathlib

77c3bfed - chore(data/zmod/basic): make `fin.comm_ring.sub` defeq to `fin.sub` (#6848)

chore(data/zmod/basic): make `fin.comm_ring.sub` defeq to `fin.sub` (#6848) This is only possible now that `fin.sub` is not saturating, and we allow `sub` and `neg` to be defined separately.