mathlib3

f8488beb - fix(algebra/group/units): splitting out `mul_one_class` for group of units (#14923)

fix(algebra/group/units): splitting out `mul_one_class` for group of units (#14923) Without this proposed change, the following example gives a `(deterministic) timeout`: ```lean import algebra.ring.basic example (R : Type*) [comm_ring R] (a b : Rˣ) : a * (b / a) = b := begin rw mul_div_cancel'_right, -- or: `simp` end ``` Co-authored-by: Jon Eugster <j.eugster@sms.ed.ac.uk>