Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-29 19:28 92af9fa8

View on Github →

feat(category_theory/limits/pullbacks): pullback self is id iff mono (#4813)

Estimated changes

Modified src/category_theory/limits/shapes/pullbacks.lean

added def category_theory.limits.pullback_cone.is_limit_mk_id_id

added theorem category_theory.limits.pullback_cone.mono_of_is_limit_mk_id_id