Theorem PiTensorProduct.norm_def

Modification history

2026-03-27 10:04
Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): switch NormedSpace instance to `projectiveSeminorm` (#35568) …
Added PiTensorProduct.norm_defView on Github →