Def IsBilinearMap.toContinuousBilinearMap

Modification history

2026-03-06 08:34
Mathlib/Topology/Algebra/Module/FiniteDimensionBilinear.lean
feat: (continuous) bilinear map (#36193) …
Added IsBilinearMap.toContinuousBilinearMapView on Github →