Theorem TensorProduct.ridIsometry_apply

Modification history

2026-07-17 21:45
Mathlib/Analysis/InnerProductSpace/TensorProduct.lean
feat(Analysis/InnerProductSpace/TensorProduct): continuous version of `TensorProduct.mk` (#40340) …
Added TensorProduct.ridIsometry_applyView on Github →