Def TensorProduct.mapInclIsometry

Modification history

2026-02-17 23:08
Mathlib/Analysis/InnerProductSpace/TensorProduct.lean
chore: bump toolchain to v4.29.0-rc1 (#35459)
Deleted TensorProduct.mapInclIsometryView 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.mapInclIsometryView on Github →