Commit 2024-11-13 20:45 b8b825aa

chore(Algebra/Ring): find a better home for RingHom.map_isUnit (#18989) This result is in the grab-bag file Ring.Hom.Basic and fits neatly into Algebra.Ring.Units. The hope is that we can eventually avoid importing Units in the file defining Module.