Theorem PiTensorProduct.projectiveSeminorm_smul_le

Modification history

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