mathlib3

b86c528d - feat(ring_theory/ideal/local_ring): API for local rings. (#17185)

feat(ring_theory/ideal/local_ring): API for local rings. (#17185) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>