Theorem Module.Projective.of_split

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.of_split View on Github →