English
For x ∈ ℝ and t ∈ ℝ, the norm of the image of t·x in AddCircle (t·p) equals |t| times the norm of the image of x in AddCircle p.
Русский
Для x ∈ ℝ и t ∈ ℝ норма образа t·x в AddCircle (t·p) равна |t| умножить на норму образа x в AddCircle p.
LaTeX
$$$$\\| (t\\,x) : \\mathrm{AddCircle}(t p) \\| = |t| \\cdot \\| x : \\mathrm{AddCircle}(p) \\|.$$$$
Lean4
@[simp]
theorem norm_coe_mul (x : ℝ) (t : ℝ) : ‖(↑(t * x) : AddCircle (t * p))‖ = |t| * ‖(x : AddCircle p)‖ :=
by
obtain rfl | ht := eq_or_ne t 0
· simp
simp only [norm_eq_infDist, ← Real.norm_eq_abs, ← infDist_smul₀ ht, smul_zero]
congr 1 with m
simp_rw [zmultiples, eq_iff_sub_mem, zsmul_eq_mul, mul_left_comm, ← smul_eq_mul, Set.range_smul]
simp [mem_smul_set_iff_inv_smul_mem₀ ht, mul_sub, ht]
