instModule — Mathlib

English

Outer measures admit a module structure over a semiring when the scalar action is defined via the underlying function.

Русский

Внешние меры образуют модуль над полем (полукольцом) когда задано скалярное действие через соответствующую функцию.

LaTeX

$$$\text{instance } \text{instModule } {R} :\ Module R (OuterMeasure\, \alpha).$$$

Lean4

instance instModule {R : Type*} [Semiring R] [Module R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] : Module R (OuterMeasure α) :=
  Injective.module R coeFnAddMonoidHom coe_fn_injective coe_smul

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