instModule — Mathlib

English

There is a module structure on Completion α over a semiring R whenever α is a module over R with Uniform continuity of scalar action.

Русский

Для Completion α существует модульная структура над полукольцом R, если α — модуль над R и скалярное действие непрерывно по униформе.

LaTeX

$$$Module\\ R\\ (Completion(\\alpha))$$$

Lean4

instance instModule [Semiring R] [Module R α] [UniformContinuousConstSMul R α] : Module R (Completion α) :=
  { (inferInstance : DistribMulAction R <| Completion α), (inferInstance : MulActionWithZero R <| Completion α) with
    add_smul := fun a b ↦
      ext' (continuous_const_smul _) ((continuous_const_smul _).add (continuous_const_smul _)) fun x ↦ by
        rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul] }

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