Commit 2023-02-21 19:30 4083ad40

View on Github →

feat: port CategoryTheory.CommSq (#2322)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/CommSq.lean

added theorem CategoryTheory.CommSq.HasLift.iff

added theorem CategoryTheory.CommSq.HasLift.iff_op

added theorem CategoryTheory.CommSq.HasLift.iff_unop

added theorem CategoryTheory.CommSq.HasLift.mk'

added def CategoryTheory.CommSq.LiftStruct.op

added def CategoryTheory.CommSq.LiftStruct.opEquiv

added def CategoryTheory.CommSq.LiftStruct.unop

added def CategoryTheory.CommSq.LiftStruct.unopEquiv

added structure CategoryTheory.CommSq.LiftStruct

added theorem CategoryTheory.CommSq.fac_left

added theorem CategoryTheory.CommSq.fac_right

added theorem CategoryTheory.CommSq.flip

added theorem CategoryTheory.CommSq.of_arrow

added theorem CategoryTheory.CommSq.op

added theorem CategoryTheory.CommSq.unop

added structure CategoryTheory.CommSq

added theorem CategoryTheory.Functor.map_commSq