uniformContinuousConstSMul — Mathlib

English

The scalar action commutes with the completion embedding under smul.

Русский

Действие скаляра коммутирует с вложением завершения под умножением.

LaTeX

$$coe_smul_adicCompletion$$

Lean4

instance uniformContinuousConstSMul : UniformContinuousConstSMul S (WithVal <| v.valuation K) :=
  by
  refine ⟨fun l ↦ ?_⟩
  simp_rw [Algebra.smul_def]
  exact (Ring.uniformContinuousConstSMul (WithVal <| v.valuation K)).uniformContinuous_const_smul _

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