Def lp.singleContinuousLinearMap

Modification history

2025-02-14 15:54

Mathlib/Analysis/Normed/Lp/lpSpace.lean

feat: `FunLike` instance for `HilbertBasis` (#21440) …

Added lp.singleContinuousLinearMap View on Github →