English
If hμ1 and hna and hx: μ(xy) = μ x μ y, then smoothingSeminorm μ hμ1 hna (x y) = smoothingSeminorm μ hμ1 hna x · smoothingSeminorm μ hμ1 hna y.
Русский
Если выполняются условия hμ1, hna и hx: μ(xy)=μx μy, то smoothingSeminorm μ hμ1 hna (xy) равно произведению сглаженных норм.
LaTeX
$$$\mathrm{smoothingSeminorm}\; μ\; hμ1\; hna\; (xy) = \mathrm{smoothingSeminorm}\; μ\; hμ1\; hna\; x \cdot \mathrm{smoothingSeminorm}\; μ\; hμ1\; hna\; y$$$
Lean4
/-- If `μ 1 ≤ 1`, `μ` is nonarchimedean, and `x` is multiplicative for `μ`, then `x` is
multiplicative for `smoothingSeminorm`. -/
theorem smoothingSeminorm_of_mul (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedean μ) {x : R}
(hx : ∀ y : R, μ (x * y) = μ x * μ y) (y : R) :
smoothingSeminorm μ hμ1 hna (x * y) = smoothingSeminorm μ hμ1 hna x * smoothingSeminorm μ hμ1 hna y :=
smoothingFun_of_map_mul_eq_mul μ hμ1 hx y
