Commit 2026-01-21 06:56 f65659be

View on Github →

feat(LinearAlgebra): make TensorProduct.finsuppLeft and friends heterobasic (#33469)

Estimated changes

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

added theorem TensorProduct.finsuppRight_tmul_single

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

modified def TensorProduct.directSumLeft

Modified Mathlib/LinearAlgebra/TensorProduct/Basis.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Submodule.lean

Modified Mathlib/RepresentationTheory/Coinvariants.lean

Modified Mathlib/RepresentationTheory/Rep.lean

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Index.lean

Modified Mathlib/RingTheory/LocalRing/Module.lean

Modified Mathlib/RingTheory/Localization/BaseChange.lean

Modified Mathlib/RingTheory/PicardGroup.lean

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangeFree.lean

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean