English
If 𝕜 is a topological ring and R acts compatibly with 𝕜, then WeakDual 𝕜 E admits a module structure over R, via the existing ContinuousLinearMap module structure.
Русский
Если 𝕜 — топологическое кольцо и R действует совместимо с 𝕜, то WeakDual 𝕜 E приобретает структуру модуля над R через существующую структуру модуля линейных отображений.
LaTeX
$$instance instModule' (R) ... : Module R (WeakDual 𝕜 E)$$
Lean4
/-- `WeakBilin B` is a `IsTopologicalAddGroup`, meaning that addition and negation are
continuous. -/
instance instIsTopologicalAddGroup [ContinuousAdd 𝕜] : IsTopologicalAddGroup (WeakBilin B)
where
toContinuousAdd := by infer_instance
continuous_neg := by
refine continuous_induced_rng.2 (continuous_pi_iff.mpr fun y => ?_)
refine cast (congr_arg _ ?_) (eval_continuous B (-y))
ext x
simp only [map_neg, Function.comp_apply, LinearMap.neg_apply]
