English
There is a scalar action of a ring R on seminorms that factors through nonnegative reals, extending the usual scalar action on the underlying seminorm.
Русский
Существует скалярное действие кольца R на семинормы, проходящее через неотрицательные числа, расширяющее обычное скалярное действие на базовую семинорму.
LaTeX
$$$\text{SMul } R (\text{Seminorm } 𝕜 E)$ with smul defined as above$$
Lean4
/-- Any action on `ℝ` which factors through `ℝ≥0` applies to a seminorm. -/
instance instSMul [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] : SMul R (Seminorm 𝕜 E) where
smul r
p :=
{ r • p.toAddGroupSeminorm with
toFun := fun x => r • p x
smul' := fun _ _ => by
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul]
rw [map_smul_eq_mul, mul_left_comm] }
