Theorem PiTensorProduct.projectiveSeminorm_add_le

Modification history

2026-04-13 12:57
Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean
style: fix whitespace (#37993) …
Modified PiTensorProduct.projectiveSeminorm_add_leView on Github →
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_add_leView on Github →
2026-03-06 09:45
Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs (#35567) …
Added PiTensorProduct.projectiveSeminorm_add_leView on Github →