Commit 2023-03-23 13:19 ddbb81cc

View on Github →

feat: port CategoryTheory.Limits.Shapes.Reflexive (#3041)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean

added theorem CategoryTheory.IsCoreflexivePair.common_retraction

added theorem CategoryTheory.IsCoreflexivePair.mk'

added theorem CategoryTheory.IsCoreflexivePair.swap

added theorem CategoryTheory.IsKernelPair.isReflexivePair

added theorem CategoryTheory.IsReflexivePair.common_section

added theorem CategoryTheory.IsReflexivePair.mk'

added theorem CategoryTheory.IsReflexivePair.swap

added theorem CategoryTheory.Limits.hasCoequalizer_of_common_section

added theorem CategoryTheory.Limits.hasEqualizer_of_common_retraction

added theorem CategoryTheory.left_comp_retraction

added theorem CategoryTheory.right_comp_retraction

added theorem CategoryTheory.section_comp_left

added theorem CategoryTheory.section_comp_right