Commit 2025-04-22 08:56 71082619

View on Github →

refactor(Algebra/Category/ModuleCat): generalize the universe of ModuleCat.enoughProjectives (#23690) Generalize the universe in the statement of ModuleCat.enoughProjectives and ModuleCat.enoughInjectives.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean

Modified Mathlib/Algebra/Category/ModuleCat/Projective.lean

modified theorem ModuleCat.projective_of_free

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

Modified scripts/nolints_prime_decls.txt