Commit 2023-09-27 21:48 0dbbdede

View on Github →

refactor(RingTheory/TensorProduct): simplify assumptions (#7403) Rather than showing agreement on all the scalars in algHomOfLinearMapTensorProduct, it suffices to show agreement on 1. This also replaces a few downstream proofs with rfl in order to make them eligible for dsimp. These results were always true by rfl, but it was easier to make this change than fix the old proofs.

Estimated changes

Modified Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Opposite.lean

Modified Mathlib/RingTheory/MatrixAlgebra.lean

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

deleted theorem PolyEquivTensor.toFunLinear_algebraMap_tmul_one

added theorem PolyEquivTensor.toFunLinear_one_tmul_one

Modified Mathlib/RingTheory/TensorProduct.lean

modified theorem Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply

modified theorem Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply

modified theorem Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply

modified theorem Algebra.TensorProduct.assoc_aux_2