Commit 2025-10-17 08:48 2528a234

View on Github →

feat(Analysis/InnerProductSpace/TensorProduct): LinearIsometry.lTensor and .rTensor (#30613) This adds the linear isometry versions of LinearMap.lTensor and LinearMap.rTensor.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

added def LinearIsometry.lTensor

added theorem LinearIsometry.lTensor_apply

added theorem LinearIsometry.lTensor_def

added def LinearIsometry.rTensor

added theorem LinearIsometry.rTensor_apply

added theorem LinearIsometry.rTensor_def

added theorem LinearIsometry.toLinearMap_lTensor

added theorem LinearIsometry.toLinearMap_rTensor

added def LinearIsometryEquiv.lTensor

added theorem LinearIsometryEquiv.lTensor_apply

added theorem LinearIsometryEquiv.lTensor_def

added def LinearIsometryEquiv.rTensor

added theorem LinearIsometryEquiv.rTensor_apply

added theorem LinearIsometryEquiv.rTensor_def

added theorem LinearIsometryEquiv.symm_lTensor

added theorem LinearIsometryEquiv.symm_rTensor

added theorem LinearIsometryEquiv.toLinearEquiv_lTensor

added theorem LinearIsometryEquiv.toLinearEquiv_rTensor

added theorem LinearIsometryEquiv.toLinearIsometry_lTensor

added theorem LinearIsometryEquiv.toLinearIsometry_rTensor

added theorem TensorProduct.congrIsometry_refl_refl

added theorem TensorProduct.mapIsometry_id_id