feat(Analysis/InnerProductSpace/TensorProduct): add TensorProduct.congrL

[TJHeeringa]

Add TensorProduct.congrL, the continuous version of TensorProduct.congr.

---

Requested in #40074 (comment).

No AI used.

• depends on: feat(Analysis/InnerProductSpace/TensorProduct): Add TensorProduct.mapL #40074
• depends on: feat(Topology/Algebra): add ContinuousLinearEquiv.ofContinuousLinearMap #40841

[github-actions]

PR summary e2feb2851b

Import changes exceeding 2%

%	File
+14.25%	Mathlib.Analysis.InnerProductSpace.TensorProduct

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.InnerProductSpace.TensorProduct	2182	2493	+311 (+14.25%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.InnerProductSpace.Coalgebra Mathlib.Analysis.InnerProductSpace.TensorProduct	311

---

Declarations diff (regex)

+ _root_.ContinuousLinearMap.adjoint_lTensor
+ _root_.ContinuousLinearMap.adjoint_rTensor
+ _root_.ContinuousLinearMap.lTensor_comp_mapL
+ _root_.ContinuousLinearMap.lTensor_comp_rTensor
+ _root_.ContinuousLinearMap.lTensor_eq_mapL
+ _root_.ContinuousLinearMap.mapL_comp_lTensor
+ _root_.ContinuousLinearMap.mapL_comp_rTensor
+ _root_.ContinuousLinearMap.rTensor_comp_lTensor
+ _root_.ContinuousLinearMap.rTensor_comp_mapL
+ _root_.ContinuousLinearMap.rTensor_eq_mapL
+ _root_.LinearIsometry.toContinuousLinearMap_lTensor
+ _root_.LinearIsometry.toContinuousLinearMap_rTensor
+ adjoint_mapL
+ commIsometry_comp_lTensor_comp_commIsometry_eq
+ commIsometry_comp_rTensor_comp_commIsometry_eq
+ congrL
+ congrL_congr
+ congrL_mul
+ congrL_pow
+ congrL_refl_refl
+ congrL_symm
+ congrL_symm_tmul
+ congrL_tmul
+ congrL_trans
+ congrL_zpow
+ lTensor
+ lTensor_add
+ lTensor_apply
+ lTensor_comp
+ lTensor_comp_commIsometry
+ lTensor_id
+ lTensor_mul
+ lTensor_neg
+ lTensor_one
+ lTensor_pow
+ lTensor_smul
+ lTensor_sub
+ lTensor_tmul
+ lTensor_zero
+ mapL
+ mapL_add_left
+ mapL_add_right
+ mapL_apply
+ mapL_comp
+ mapL_comp_commIsometry
+ mapL_id_id
+ mapL_mul
+ mapL_pow
+ mapL_smul_left
+ mapL_smul_right
+ mapL_tmul
+ mapL_zero_left
+ mapL_zero_right
+ norm_lTensor_le
+ norm_mapL_le
+ norm_rTensor_le
+ ofContinuousLinear
+ ofContinuousLinear_apply
+ ofContinuousLinear_symm_apply
+ ofContinuousLinear_symm_toContinuousLinearMap
+ ofContinuousLinear_toLinearMap
+ rTensor
+ rTensor_add
+ rTensor_apply
+ rTensor_comp
+ rTensor_comp_commIsometry
+ rTensor_id
+ rTensor_mul
+ rTensor_neg
+ rTensor_one
+ rTensor_pow
+ rTensor_smul
+ rTensor_sub
+ rTensor_tmul
+ rTensor_zero
+ toContinuousLinearMap_congrL
+ toContinuousLinearMap_mapIsometry
+ toLinearMap_congrL
+ toLinearMap_lTensor
+ toLinearMap_mapL
+ toLinearMap_rTensor
+ toLinearMap_toContinuousLinearMap

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e2feb28).

• +83 new declarations
• −0 removed declarations

+ContinuousLinearEquiv.ofContinuousLinear
+ContinuousLinearEquiv.ofContinuousLinear.congr_simp
+ContinuousLinearEquiv.ofContinuousLinear_apply
+ContinuousLinearEquiv.ofContinuousLinear_symm_apply
+ContinuousLinearEquiv.ofContinuousLinear_symm_toContinuousLinearMap
+ContinuousLinearEquiv.ofContinuousLinear_toLinearMap
+ContinuousLinearMap.adjoint_lTensor
+ContinuousLinearMap.adjoint_rTensor
+ContinuousLinearMap.commIsometry_comp_lTensor_comp_commIsometry_eq
+ContinuousLinearMap.commIsometry_comp_rTensor_comp_commIsometry_eq
+ContinuousLinearMap.lTensor
+ContinuousLinearMap.lTensor_add
+ContinuousLinearMap.lTensor_apply
+ContinuousLinearMap.lTensor_comp
+ContinuousLinearMap.lTensor_comp_commIsometry
+ContinuousLinearMap.lTensor_comp_mapL
+ContinuousLinearMap.lTensor_comp_rTensor
+ContinuousLinearMap.lTensor_eq_mapL
+ContinuousLinearMap.lTensor_id
+ContinuousLinearMap.lTensor_mul
+ContinuousLinearMap.lTensor_neg
+ContinuousLinearMap.lTensor_one
+ContinuousLinearMap.lTensor_pow
+ContinuousLinearMap.lTensor_smul
+ContinuousLinearMap.lTensor_sub
+ContinuousLinearMap.lTensor_tmul
+ContinuousLinearMap.lTensor_zero
+ContinuousLinearMap.mapL_comp_lTensor
+ContinuousLinearMap.mapL_comp_rTensor
+ContinuousLinearMap.norm_lTensor_le
+ContinuousLinearMap.norm_rTensor_le
+ContinuousLinearMap.rTensor
+ContinuousLinearMap.rTensor_add
+ContinuousLinearMap.rTensor_apply
+ContinuousLinearMap.rTensor_comp
+ContinuousLinearMap.rTensor_comp_commIsometry
+ContinuousLinearMap.rTensor_comp_lTensor
+ContinuousLinearMap.rTensor_comp_mapL
+ContinuousLinearMap.rTensor_eq_mapL
+ContinuousLinearMap.rTensor_id
+ContinuousLinearMap.rTensor_mul
+ContinuousLinearMap.rTensor_neg
+ContinuousLinearMap.rTensor_one
+ContinuousLinearMap.rTensor_pow
+ContinuousLinearMap.rTensor_smul
+ContinuousLinearMap.rTensor_sub
+ContinuousLinearMap.rTensor_tmul
+ContinuousLinearMap.rTensor_zero
+ContinuousLinearMap.toLinearMap_lTensor
+ContinuousLinearMap.toLinearMap_rTensor
+LinearIsometry.toContinuousLinearMap_lTensor
+LinearIsometry.toContinuousLinearMap_rTensor
+LinearIsometry.toLinearMap_toContinuousLinearMap
+TensorProduct.adjoint_mapL
+TensorProduct.congrL
+TensorProduct.congrL_congr
+TensorProduct.congrL_mul
+TensorProduct.congrL_pow
+TensorProduct.congrL_refl_refl
+TensorProduct.congrL_symm
+TensorProduct.congrL_symm_tmul
+TensorProduct.congrL_tmul
+TensorProduct.congrL_trans
+TensorProduct.congrL_zpow
+TensorProduct.mapL
+TensorProduct.mapL_add_left
+TensorProduct.mapL_add_right
+TensorProduct.mapL_apply
+TensorProduct.mapL_comp
+TensorProduct.mapL_comp_commIsometry
+TensorProduct.mapL_id_id
+TensorProduct.mapL_mul
+TensorProduct.mapL_pow
+TensorProduct.mapL_smul_left
+TensorProduct.mapL_smul_right
+TensorProduct.mapL_tmul
+TensorProduct.mapL_zero_left
+TensorProduct.mapL_zero_right
+TensorProduct.norm_mapL_le
+TensorProduct.toContinuousLinearMap_congrL
+TensorProduct.toContinuousLinearMap_mapIsometry
+TensorProduct.toLinearMap_congrL
+TensorProduct.toLinearMap_mapL

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit e2feb2851b
Reference commit fbfd7f57b6

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Analysis/InnerProductSpace/TensorProduct): Add TensorProduct.mapL #40074
• feat(Topology/Algebra): add ContinuousLinearEquiv.ofContinuousLinearMap #40841
  By Dependent Issues (🤖). Happy coding!