instMulAction — Mathlib

English

There is a natural scalar action of a monoid R on the set of seminorms on E, defined by (r · p)(x) = r · p(x).

Русский

Существует естественное скалярное действие моноида R на множество полунорм p на E, задающееся как (r · p)(x) = r · p(x).

LaTeX

$$$ (r \cdot p)(x) = r \cdot p(x) $$$

Lean4

instance instMulAction [Monoid R] [MulAction R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] : MulAction R (Seminorm 𝕜 E) :=
  DFunLike.coe_injective.mulAction _ (by intros; rfl)

Похожие утверждения