feat(ring_theory/multiplicity): Multiplicity with units (#6729)
Renames `multiplicity.multiplicity_unit` into `multiplicity.is_unit_left`.
Adds :
* `multiplicity.is_unit_right`
* `multiplicity.unit_left`
* `multiplicity.unit_right`
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
