instSMulCommClassOfUniformContinuousConstSMul

English

If M,N act on X with SMulCommClass and UniformContinuousConstSMul, then SMulCommClass M N (Completion X).

Русский

Если M,N действуют на X и выполняется свойство SMulCommClass, и применяется равномерно непрерывное константное умножение, то SMulCommClass на Completion X выполняется.

LaTeX

$$$SMulCommClass\\ M\\ N\\ (\\mathrm{Completion}(X))$$$

Lean4

@[to_additive]
instance [SMul N X] [SMulCommClass M N X] [UniformContinuousConstSMul M X] [UniformContinuousConstSMul N X] :
    SMulCommClass M N (Completion X) :=
  ⟨fun m n x =>
    by
    have hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x := rfl
    have hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x := rfl
    rw [hmn, hnm, map_comp, map_comp]
    · exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _))
    repeat' exact uniformContinuous_const_smul _⟩

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