Def lp.singleContinuousAddMonoidHom

Modification history

2025-02-14 15:54
Mathlib/Analysis/Normed/Lp/lpSpace.lean
feat: `FunLike` instance for `HilbertBasis` (#21440) …
Added lp.singleContinuousAddMonoidHomView on Github →