Commit 2026-07-09 14:40 89a18ed2

View on Github →

chore: move dualDistribEquiv (#41535) This is in prevision of #41479 redefining it in terms of homTensorHomEquiv. Extracted by Claude Opus from #41479 Assisted-by: Claude Opus 4.8

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

added theorem TensorProduct.dualDistribInvOfBasis_apply

added theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse

added theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse

Modified Mathlib/LinearAlgebra/Dual/Lemmas.lean

deleted theorem TensorProduct.dualDistribInvOfBasis_apply

deleted theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_left_inverse

deleted theorem TensorProduct.dualDistrib_dualDistribInvOfBasis_right_inverse