Theorem IsProjective.iff_projective

Modification history

2025-06-03 11:40
Mathlib/Algebra/Category/ModuleCat/Projective.lean
refactor(Algebra/Module/Projective): generalize universes (#24697) …
Modified IsProjective.iff_projectiveView on Github →
2023-05-20 10:55
Mathlib/Algebra/Category/ModuleCat/Projective.lean
feat: port Algebra.Category.ModuleCat.Projective (#3964) …
Added IsProjective.iff_projectiveView on Github →