English
If s is balanced and 𝕜 is a normed field, then gauge s (‖r‖ • x) = gauge s (r • x).
Русский
Если s сбалансировано и 𝕜 — нормированное поле, то gauge s (‖r‖ • x) = gauge s (r • x).
LaTeX
$$$$\\mathrm{gauge}(s, \\|r\\| \\cdot x) = \\mathrm{gauge}(s, r \\cdot x).$$$$
Lean4
theorem gauge_norm_smul (hs : Balanced 𝕜 s) (r : 𝕜) (x : E) : gauge s (‖r‖ • x) = gauge s (r • x) :=
by
unfold gauge
congr with θ
rw [@RCLike.real_smul_eq_coe_smul 𝕜]
refine and_congr_right fun hθ => (hs.smul _).smul_mem_iff ?_
rw [RCLike.norm_ofReal, abs_norm]