Commit 2023-11-02 21:53 7f7a1f04

View on Github →

chore(RingTheory/TensorProduct): missing trivial lemmas (#8120) This also tweaks some argument explicitness, and removes unnecessary type ascriptions

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.rid_symm_apply

Modified Mathlib/RingTheory/TensorProduct.lean

added theorem Algebra.TensorProduct.assoc_symm_tmul

added theorem Algebra.TensorProduct.comm_symm

added theorem Algebra.TensorProduct.comm_symm_tmul

added theorem Algebra.TensorProduct.lid_symm_apply

modified theorem Algebra.TensorProduct.lid_tmul

added theorem Algebra.TensorProduct.rid_symm_apply