Theorem PiTensorProduct.norm_eval_le_projectiveSeminorm
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.norm_eval_le_projectiveSeminormView on Github →2024-03-24 20:38
Mathlib/Analysis/NormedSpace/PiTensorProduct/ProjectiveSeminorm.lean
feat(Analysis/NormedSpace/PiTensorProduct/{InjectiveNorm, ProjectiveNorm}, LinearAlgebra/PiTensorProduct): define the injective and projective norms on `PiTensorProduct` and prove the universal property of the first one (#11534) …
Added PiTensorProduct.norm_eval_le_projectiveSeminormView on Github →