Commit 2026-07-17 21:45 4851ebd9

View on Github →

feat(Analysis/InnerProductSpace/TensorProduct): continuous version of TensorProduct.mk (#40340) and isometric version of TensorProduct.rid.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

added theorem TensorProduct.coe_mkL_apply

added theorem TensorProduct.commIsometry_trans_lidIsometry

added theorem TensorProduct.commIsometry_trans_ridIsometry

added theorem TensorProduct.continuous_tmul

added theorem TensorProduct.enorm_rid

added theorem TensorProduct.inner_rid_rid

modified theorem TensorProduct.lidIsometry_apply

added theorem TensorProduct.lidIsometry_eq_ridIsometry

modified theorem TensorProduct.lidIsometry_symm_apply

added theorem TensorProduct.mkL_apply_apply

modified theorem TensorProduct.nnnorm_lid

added theorem TensorProduct.nnnorm_rid

modified theorem TensorProduct.norm_lid

added theorem TensorProduct.norm_rid

added theorem TensorProduct.ridIsometry_apply

added theorem TensorProduct.symm_ridIsometry_apply

added theorem TensorProduct.toContinuousLinearMap_symm_lidIsometry

added theorem TensorProduct.toContinuousLinearMap_symm_ridIsometry

added theorem TensorProduct.toLinearEquiv_ridIsometry

added theorem TensorProduct.toLinearMap_mkL_apply

added theorem TensorProduct.toLinearMap₁₂_mkL

Modified Mathlib/LinearAlgebra/TensorProduct/Associator.lean

added theorem TensorProduct.lid_comm

added theorem TensorProduct.rid_comm