Mathlib v4.35: isUnit_of_mul_eq_one is IsUnit.of_mul_eq_one now

On Mathlib v4.35.0, isUnit_of_mul_eq_one and isUnit_of_mul_eq_one_right are unknown identifiers (deleted, with no deprecation hint). The replacements are IsUnit.of_mul_eq_one (b) (h : a * b = 1) : IsUnit a and IsUnit.of_mul_eq_one_right (a) (h : a * b = 1) : IsUnit b. They, isUnit_iff_exists_inv, Units.mkOfMulEqOne and mul_eq_one_comm now assume [Monoid M] [IsDedekindFiniteMonoid M] instead of a commutative monoid. Every CommMonoid gets that instance by inferInstance (checked for ZMod n), so commutative code only needs the rename. In the dvd family, isUnit_of_dvd_one still exists under its old root name (IsUnit.of_dvd_one does not), so the rename was not applied uniformly; #check before you sed.