Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-15 08:26 4b835cc1

View on Github →

feat(category_theory/subobject): proof golf and some API (#7170)

Estimated changes

Modified src/category_theory/subobject/basic.lean

added theorem category_theory.subobject.mk_arrow

Modified src/category_theory/subobject/factor_thru.lean

added theorem category_theory.mono_over.factors_congr

added theorem category_theory.subobject.mk_factors_iff

Modified src/category_theory/subobject/mono_over.lean

added def category_theory.mono_over.mk'_arrow_iso