instMulActionOfUniformContinuousConstSMul

English

The completion carries a multiplicative action of M extending the original action on X, with the usual associativity and identity properties.

Русский

Дополнение X имеет бинарное умножение M, продолжающее исходное действие на X, с обычной связностью и единицей.

LaTeX

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

Lean4

@[to_additive]
noncomputable instance [Monoid M] [MulAction M X] [UniformContinuousConstSMul M X] : MulAction M (Completion X)
    where
  smul := (· • ·)
  one_smul := ext' (continuous_const_smul _) continuous_id fun a => by rw [← coe_smul, one_smul]
  mul_smul x
    y :=
    ext' (continuous_const_smul _) ((continuous_const_smul _).const_smul _) fun a => by simp only [← coe_smul, mul_smul]

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