Commit 2024-04-26 18:08 728940e9

View on Github →

feat: Generalize Basis.tensorProduct to heterobasic version (#11844) In order to achieve this, finsuppTensorFinsupp and TensorProduct.directSum are also heterobasic now.

Estimated changes

Modified Mathlib/Algebra/Lie/TensorProduct.lean

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

added def finsuppTensorFinsupp

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basis.lean

modified def Basis.tensorProduct

Modified Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean