Theorem PiTensorProduct.opNorm_mapL

Modification history

2026-06-18 10:58
Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): deprecate `injectiveSeminorm` (#35569) …
Added PiTensorProduct.opNorm_mapLView on Github →