Theorem Module.Projective.iff_split_of_projective

Modification history

2024-06-05 18:56
Mathlib/Algebra/Module/Projective.lean
feat(Algebra/Module/Projective): Tensor product of projective modules (#13091)
Added Module.Projective.iff_split_of_projectiveView on Github →