Commit 2024-03-26 16:49 6983af43

View on Github →

chore(CategoryTheory): add some trivial API lemmas for Zag and Zigzag (#11696)

Estimated changes

Modified Mathlib/CategoryTheory/IsConnected.lean

added theorem CategoryTheory.Zag.of_hom

added theorem CategoryTheory.Zag.of_inv

added theorem CategoryTheory.Zag.refl

added theorem CategoryTheory.Zag.symm

added theorem CategoryTheory.Zigzag.of_hom

added theorem CategoryTheory.Zigzag.of_hom_hom

added theorem CategoryTheory.Zigzag.of_hom_inv

added theorem CategoryTheory.Zigzag.of_inv

added theorem CategoryTheory.Zigzag.of_inv_hom

added theorem CategoryTheory.Zigzag.of_inv_inv

added theorem CategoryTheory.Zigzag.of_zag

added theorem CategoryTheory.Zigzag.of_zag_trans

added theorem CategoryTheory.Zigzag.trans