instMulActionWithZeroOfUniformContinuousConstSMul

Mathlib.Topology.Algebra.GroupCompletion

URI: https://scilib.ai/kg/mathlib#UniformSpace.Completion.instMulActionWithZeroOfUniformContinuousConstSMul

Lean4

instance [UniformSpace α] [MonoidWithZero M] [Zero α] [MulActionWithZero M α] [UniformContinuousConstSMul M α] :
    MulActionWithZero M (Completion α) :=
  {
    (inferInstance :
      MulAction M <|
        Completion
          α) with
    smul_zero := fun r ↦ by rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
    zero_smul := ext' (continuous_const_smul _) continuous_const fun a ↦ by rw [← coe_smul, zero_smul, coe_zero] }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru