Theorem ContinuousLinearMap.evalL_apply

Modification history

2026-09-29 15:02
Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean
feat: introduce an IsNormableSpace class (#42983) …
Deleted ContinuousLinearMap.evalL_applyView on Github →
2026-03-06 08:34
Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean
feat: (continuous) bilinear map (#36193) …
Added ContinuousLinearMap.evalL_applyView on Github →