English
Left multiplication by b maps the sphere around a with radius r to the sphere around a/b with radius r.
Русский
Левая передвижка на b переносит сферу вокруг a радиуса r в сферу вокруг a/b радиуса r.
LaTeX
$$$\displaystyle (b\cdot\,\cdot)^{-1}'\mathrm{sphere}\,a\,r = \mathrm{sphere}\,(a/b)\,r$$$
Lean4
@[to_additive (attr := simp)]
theorem preimage_mul_sphere (a b : E) (r : ℝ) : (b * ·) ⁻¹' sphere a r = sphere (a / b) r :=
by
ext c
simp only [Set.mem_preimage, mem_sphere_iff_norm', div_div_eq_mul_div, mul_comm]