Theorem LinearIsometryEquiv.toLinearEquiv_rTensor

Modification history

2025-10-17 08:48
Mathlib/Analysis/InnerProductSpace/TensorProduct.lean
feat(Analysis/InnerProductSpace/TensorProduct): `LinearIsometry.lTensor` and `.rTensor` (#30613) …
Added LinearIsometryEquiv.toLinearEquiv_rTensorView on Github →