Commit 2025-05-08 21:19 0df43928

View on Github →

feat: homOfEq lemmas (#24538)

  • Add lemmas for the symmetry of Quiver.homOfEq
  • Add lemmas establishing HEq of Quiver.homOfEq f ... with the original morphism f

Estimated changes

added theorem Quiver.eq_homOfEq_iff
added theorem Quiver.homOfEq_eq_iff
added theorem Quiver.homOfEq_heq