instContinuousSMul — Mathlib

English

There is a canonical continuous scalar multiplication on the space of continuous alternating maps by the base field 𝕜, making it a 𝕜‑module in the natural way.

Русский

Существует каноническое непрерывное умножение на скаляры 𝕜 на пространстве непрерывных чередующихся отображений, превращающее его в 𝕜‑модулял при естественном определении.

LaTeX

$$$[ContinuousSMul\\; 𝕜\\; (E [⋀^ι]→L[𝕜] F)]$$$

Lean4

instance instContinuousSMul [ContinuousSMul 𝕜 F] : ContinuousSMul 𝕜 (E [⋀^ι]→L[𝕜] F) :=
  isEmbedding_toContinuousMultilinearMap.continuousSMul continuous_id rfl

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