Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-15 08:11 53f6d687

View on Github →

feat(category_theory/preadditive) : definition of injective resolution (#12641) This pr is splitted from #12545. This pr contains the definition of:

  • InjectiveResolution;
  • has_injective_resolution and has_injective_resolutions;
  • injective object has injective resolution.

Estimated changes