instContinuousConstSMul — Mathlib

English

There is a continuous scalar action of the base field 𝕜 on ContinuousMultilinearMap 𝕜 E F.

Русский

Существует непрерывное скалярное действие поля 𝕜 на ContinuousMultilinearMap 𝕜 E F.

LaTeX

$$UniformContinuous (ContinuousMultilinearMap.funLike.coe)$$

Lean4

instance instContinuousConstSMul {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass 𝕜 M F]
    [ContinuousConstSMul M F] : ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F) :=
  by
  letI := IsTopologicalAddGroup.toUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  infer_instance

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