Theorem PiLp.normSMulClassSeminormedAddCommGroupToPi

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.normSMulClassSeminormedAddCommGroupToPiView on Github →