Theorem PiLp.isBoundedSMulSeminormedAddCommGroupToPi

Modification history

2025-11-21 15:15
Mathlib/Analysis/Normed/Lp/PiLp.lean
perf: de-instance some WithLp norm structures used for type synonyms (#31819) …
Added PiLp.isBoundedSMulSeminormedAddCommGroupToPiView on Github →