Commit 2023-09-08 11:01 dd9279a5

View on Github →

chore(*/TensorProduct): missing functorial lemmas (#6781) This adds missing map_id, map_comp, congr_refl, congr_trans, and congr_symm lemmas.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.congr_mul

added theorem TensorProduct.AlgebraTensorModule.congr_one

added theorem TensorProduct.AlgebraTensorModule.congr_refl

added theorem TensorProduct.AlgebraTensorModule.congr_symm

added theorem TensorProduct.AlgebraTensorModule.congr_trans

added theorem TensorProduct.AlgebraTensorModule.map_comp

added theorem TensorProduct.AlgebraTensorModule.map_id

Modified Mathlib/RingTheory/TensorProduct.lean

added theorem Algebra.TensorProduct.congr_refl

added theorem Algebra.TensorProduct.congr_symm

added theorem Algebra.TensorProduct.congr_trans

added theorem Algebra.TensorProduct.map_comp

added theorem Algebra.TensorProduct.map_id