instModule' — Mathlib

English

The weak space carries a module structure over the base field 𝕜 via the flipped dual pairing.

Русский

Слабое пространство наделено структурой модуля над полем 𝕜 посредством перевернутой двойственной пары.

LaTeX

$$$\\text{WeakSpace } 𝕜 E\\text{ is a } 𝕜\\text{-module}$$$

Lean4

instance instModule' [CommSemiring 𝕝] [Module 𝕝 E] : Module 𝕝 (WeakSpace 𝕜 E) :=
  WeakBilin.instModule' (topDualPairing 𝕜 E).flip

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