Def LinearMap.mkContinuous₂OfExists

Modification history

2026-09-29 15:02
Mathlib/Analysis/Normed/Operator/Bilinear.lean
feat: introduce an IsNormableSpace class (#42983) …
Added LinearMap.mkContinuous₂OfExistsView on Github →