Commit 2025-03-02 22:29 b22c448b

View on Github →

refactor(RingTheory/TensorProduct): reorder variables to match the module version (#22444) This changes the types such the variables are in order in the conclusion, rather than the assumptions. Now Algebra.TensorProduct.map has the type arguments in the same order as TensorProduct.AlgebraTensorModule.map and TensorProduct.map, and same for congr.

Estimated changes

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

modified def Algebra.TensorProduct.congr

modified theorem Algebra.TensorProduct.congr_apply

modified theorem Algebra.TensorProduct.congr_refl

modified theorem Algebra.TensorProduct.congr_symm

modified theorem Algebra.TensorProduct.congr_symm_apply

modified theorem Algebra.TensorProduct.congr_toLinearEquiv

modified theorem Algebra.TensorProduct.congr_trans

modified def Algebra.TensorProduct.map

modified theorem Algebra.TensorProduct.map_comp

modified theorem Algebra.TensorProduct.map_comp_id

modified theorem Algebra.TensorProduct.map_comp_includeLeft

modified theorem Algebra.TensorProduct.map_comp_includeRight

modified theorem Algebra.TensorProduct.map_id

modified theorem Algebra.TensorProduct.map_id_comp

modified theorem Algebra.TensorProduct.map_range

modified theorem Algebra.TensorProduct.map_restrictScalars_comp_includeRight

modified theorem Algebra.TensorProduct.map_tmul