Theorem Module.Projective.of_equiv

Modification history

2026-02-25 05:21
Mathlib/Algebra/Module/Projective.lean
refactor(Algebra/*): generalize `of_ringEquiv` lemmas (#35351) …
Modified Module.Projective.of_equivView on Github →
2024-06-05 18:56
Mathlib/Algebra/Module/Projective.lean
feat(Algebra/Module/Projective): Tensor product of projective modules (#13091)
Added Module.Projective.of_equivView on Github →