Theorem PiTensorProduct.nonempty_lifts

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) …