feat(Algebra/Order): multiplicative versions of lemmas on (pre)images of intervals under group operations (leanprover-community#34561)

Currently, `Mathlib/Algebra/Order/Group/Pointwise/Interval.lean` contains lemmas about (pre)images of intervals under group operations only for additive groups. This PR adds multiplicative versions and derives the additive ones via `to_additive`.

It also renames lemmas about `GroupWithZero` (e.g. `preimage_const_mul_Ico` → `preimage_const_mul_Ico₀`) to avoid name collisions.

Author: vasnesterov