mathlib3

18d4e519 - chore(algebra/ring/basic): weaken ring.inverse to only require monoid_with_zero (#6603)

chore(algebra/ring/basic): weaken ring.inverse to only require monoid_with_zero (#6603) Split from #5539 because I actually want to use this, and the PR is large and stalled. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>