Commit 2026-07-12 11:31 c0cbc05a

View on Github →

chore(LinearAlgebra/TensorProduct/Map): add symm_lTensor and symm_rTensor (#41550) This PR adds 2 simp lemmas about pulling an equivalence through a tensor product of modules, and deprecates 4 simp lemmas that become solvable by simp.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Map.lean

modified theorem LinearEquiv.coe_lTensor_symm

modified theorem LinearEquiv.coe_rTensor_symm

modified theorem LinearEquiv.lTensor_symm_tmul

modified theorem LinearEquiv.rTensor_symm_tmul

added theorem LinearEquiv.symm_lTensor

added theorem LinearEquiv.symm_rTensor

Modified Mathlib/RingTheory/Coalgebra/CoassocSimps.lean