Mathlib Changelog
v4
Changelog
About
Github
Theorem
lp.singleContinuousLinearMap_apply
Modification history
2025-03-12 08:26
Mathlib/Analysis/Normed/Lp/lpSpace.lean
chore(whitespace): more changes (#22853) …
Modified
lp.singleContinuousLinearMap_apply
View on Github →
2025-02-14 15:54
Mathlib/Analysis/Normed/Lp/lpSpace.lean
feat: `FunLike` instance for `HilbertBasis` (#21440) …
Added
lp.singleContinuousLinearMap_apply
View on Github →