Commit 2023-04-17 16:37 bd60da1b

View on Github →

feat: port CategoryTheory.Subobject.FactorThru (#3445)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subobject/FactorThru.lean

added def CategoryTheory.MonoOver.Factors

added def CategoryTheory.MonoOver.factorThru

added theorem CategoryTheory.MonoOver.factors_congr

added def CategoryTheory.Subobject.Factors

added def CategoryTheory.Subobject.factorThru

added theorem CategoryTheory.Subobject.factorThru_add

added theorem CategoryTheory.Subobject.factorThru_add_sub_factorThru_left

added theorem CategoryTheory.Subobject.factorThru_add_sub_factorThru_right

added theorem CategoryTheory.Subobject.factorThru_arrow

added theorem CategoryTheory.Subobject.factorThru_comp_arrow

added theorem CategoryTheory.Subobject.factorThru_eq_zero

added theorem CategoryTheory.Subobject.factorThru_mk_self

added theorem CategoryTheory.Subobject.factorThru_ofLe

added theorem CategoryTheory.Subobject.factorThru_right

added theorem CategoryTheory.Subobject.factorThru_self

added theorem CategoryTheory.Subobject.factorThru_zero

added theorem CategoryTheory.Subobject.factors_add

added theorem CategoryTheory.Subobject.factors_comp_arrow

added theorem CategoryTheory.Subobject.factors_iff

added theorem CategoryTheory.Subobject.factors_left_of_factors_add

added theorem CategoryTheory.Subobject.factors_of_factors_right

added theorem CategoryTheory.Subobject.factors_of_le

added theorem CategoryTheory.Subobject.factors_right_of_factors_add

added theorem CategoryTheory.Subobject.factors_self

added theorem CategoryTheory.Subobject.factors_zero

added theorem CategoryTheory.Subobject.mk_factors_iff

added theorem CategoryTheory.Subobject.mk_factors_self