Def ContinuousLinearMapWOT.addEquiv

Modification history

2026-08-10 23:43

Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

feat: generalize transfer instance type class assumptions (#42291) …

Modified ContinuousLinearMapWOT.addEquiv View on Github →

2026-04-23 17:52

Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean

feat: turn `ContinuousLinearMapWOT` into a structure (#37905) …

Added ContinuousLinearMapWOT.addEquiv View on Github →