Theorem FreeAddMonoid.toPiTensorProduct

Modification history

2024-03-24 20:38

Mathlib/LinearAlgebra/PiTensorProduct.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 FreeAddMonoid.toPiTensorProduct View on Github →