Zulip Chat Archive
Stream: general
Topic: hom_of_le / le_of_hom
Johan Commelin (May 19 2021 at 12:22):
What do people think of defining quiver.hom.le and has_le.le.hom as alternatives to le_of_hom and hom_of_le?
Johan Commelin (May 19 2021 at 12:22):
Is that dot.abuse?
Adam Topaz (May 19 2021 at 12:44):
Can we have both?
Scott Morrison (May 19 2021 at 23:15):
No objection.
Johan Commelin (May 20 2021 at 04:00):
Last updated: Dec 20 2023 at 11:08 UTC