Theorem TensorProduct.nnnorm_lid

Modification history

2026-07-17 21:45

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

feat(Analysis/InnerProductSpace/TensorProduct): continuous version of `TensorProduct.mk` (#40340) …

Modified TensorProduct.nnnorm_lid View on Github →

2025-10-16 16:17

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

feat(Analysis/InnerProductSpace): define the inner product on tensor products (#27228) …

Added TensorProduct.nnnorm_lid View on Github →