instIsCentralScalar — Mathlib

English

If M acts on X with IsCentralScalar M X and UniformContinuousConstSMul, then IsCentralScalar M (Completion X).

Русский

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

LaTeX

$$$\\text{IsCentralScalar } M\\ (\\mathrm{Completion}(X))$$$

Lean4

@[to_additive]
instance [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] : IsCentralScalar M (Completion X) :=
  ⟨fun c a => (congr_arg fun f => Completion.map f a) <| funext (op_smul_eq_smul c)⟩

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