Def ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM

Modification history

2024-11-02 18:11
Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
chore(ContinuousLinearMapWOT): generalize and golf (#17492)
Added ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLMView on Github →