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 <da64e90baec5d084ce3d8e05f3b022ae6d118ff5@gmail.com>

leanprover-community/mathlib,leanprover-community/mathlib