Theorem PiTensorProduct.liftIsometry_comp_mapL
Modification history
2026-06-18 10:58
Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean
refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): deprecate `injectiveSeminorm` (#35569) …
Modified PiTensorProduct.liftIsometry_comp_mapLView on Github →2024-03-24 20:38
Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.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.liftIsometry_comp_mapLView on Github →