Commit 2023-09-28 19:35 b2d41523

View on Github →

chore(CategoryTheory): rename Cofan.proj as Cofan.inj (#7406) This PR renames the "injections" of a cofan as Cofan.inj. The previous name Cofan.proj was confusing.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

added theorem CategoryTheory.Limits.Bicone.toCocone_inj

deleted theorem CategoryTheory.Limits.Bicone.toCocone_proj

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

added def CategoryTheory.Limits.Cofan.inj

deleted def CategoryTheory.Limits.Cofan.proj

added theorem CategoryTheory.Limits.cofan_mk_inj

deleted theorem CategoryTheory.Limits.cofan_mk_proj