Def LinearIsometry.rTensor

Modification history

2026-02-17 23:08

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

chore: bump toolchain to v4.29.0-rc1 (#35459)

Deleted LinearIsometry.rTensor View on Github →

2025-10-17 08:48

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

feat(Analysis/InnerProductSpace/TensorProduct): `LinearIsometry.lTensor` and `.rTensor` (#30613) …

Added LinearIsometry.rTensor View on Github →