Theorem lp.toAddMonoidHom_linearMapOfLE

Modification history

2026-03-30 20:46
Mathlib/Analysis/Normed/Lp/lpSpace.lean
feat: add missing API for `lp E p` (#35152) …
Added lp.toAddMonoidHom_linearMapOfLEView on Github →