Theorem Module.Projective.of_ringEquiv

Modification history

2026-02-25 05:21
Mathlib/Algebra/Module/Projective.lean
refactor(Algebra/*): generalize `of_ringEquiv` lemmas (#35351) …
Deleted Module.Projective.of_ringEquivView on Github →
2024-10-29 13:01
Mathlib/Algebra/Module/Projective.lean
feat(RingTheory/*): prerequisites to the locality of projectivity (#18264) …
Added Module.Projective.of_ringEquivView on Github →