instDistribMulActionOfUniformContinuousConstSMul

English

If a monoid M acts on α by uniform continuous smul, then Completion α carries a distributionally compatible M-action, i.e., it is a DistribMulAction.

Русский

Если моноид M действует на α плавно по униформной теме, то Completion α имеет совместимое действие M, то есть является DistribMulAction.

LaTeX

$$$\\mathrm{DistribMulAction}(M, \\mathrm{Completion}(\\alpha))$$$

Lean4

instance {M} [Monoid M] [DistribMulAction M α] [UniformContinuousConstSMul M α] : DistribMulAction M (Completion α) :=
  {
    (inferInstance :
      MulAction M <|
        Completion
          α) with
    smul_add := fun r x y ↦
      induction_on₂ x y
        (isClosed_eq ((continuous_fst.add continuous_snd).const_smul _)
          ((continuous_fst.const_smul _).add (continuous_snd.const_smul _)))
        fun a b ↦ by simp only [← coe_add, ← coe_smul, smul_add]
    smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, smul_zero r] }

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