Def ContinuousLinearMap.evalL

Modification history

2026-09-29 15:02

Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean

feat: introduce an IsNormableSpace class (#42983) …

Deleted ContinuousLinearMap.evalL View on Github →

2026-03-06 08:34

Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean

feat: (continuous) bilinear map (#36193) …

Added ContinuousLinearMap.evalL View on Github →