instDistribMulAction — Mathlib

English

There is a distributive action of a monoid R on the set Seminorm 𝕜 E, compatible with the given action on Real and NNReal via IsScalarTower.

Русский

Существуют распределенные действия моноида R на множество Seminorm 𝕜 E, совместимые с действием на Real и NNReal через IsScalarTower.

LaTeX

$$$ \text{DistribMulAction } R \ Seminorm 𝕜 E $$$

Lean4

instance instDistribMulAction [Monoid R] [DistribMulAction R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] :
    DistribMulAction R (Seminorm 𝕜 E) :=
  (coeFnAddMonoidHom_injective 𝕜 E).distribMulAction _ (by intros; rfl)

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