Commit 2024-06-05 18:56 193abd2f

View on Github →

feat(Algebra/Module/Projective): Tensor product of projective modules (#13091)

Estimated changes

Modified Mathlib/Algebra/Module/Projective.lean

added theorem Module.Projective.iff_split

added theorem Module.Projective.iff_split_of_projective

added theorem Module.Projective.of_equiv

added theorem Module.Projective.of_split

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Basis.lean