mathlib3

d1accf4f - chore(ring_theory/ideal/local_ring): use `derive` for more consistent instances (#17468)

chore(ring_theory/ideal/local_ring): use `derive` for more consistent instances (#17468) Many definitions are now computable due to the shortcut `ring` and `comm_ring` instances. The new `algebra` instance now avoids diamonds in `smul` caused by `to_algebra`.