Commit 2024-03-24 20:38 1f8fea7d

View on Github →

feat: ind-objects are closed under isomorphism (#11623)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Indization/IndObject.lean

added def CategoryTheory.Limits.IndObjectPresentation.ofCocone

added theorem CategoryTheory.Limits.IsIndObject.iff_of_iso

added theorem CategoryTheory.Limits.IsIndObject.map