Def PiTensorProduct.projectiveSeminormAux

Modification history

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.projectiveSeminormAux View on Github →