Theorem TensorProduct.toContinuousLinearMap_symm_ridIsometry

Modification history

2026-07-17 21:45

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

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

Added TensorProduct.toContinuousLinearMap_symm_ridIsometry View on Github →