Zulip Chat Archive
Stream: mathlib4
Topic: monotoneOn_univ
Yaël Dillies (Dec 03 2022 at 17:04):
Shouldn't docs4#monotoneOn_univ be renamed to monotone_on_univ as it's a lemma?
Scott Morrison (Dec 03 2022 at 17:11):
No. CamelCased names get turned into camelCase when used in lemmas, but no underscores are inserted.
Yaël Dillies (Dec 03 2022 at 17:12):
So LT gets turned in lT? :thinking:
Jireh Loreaux (Dec 03 2022 at 17:15):
No, upper cased abbreviations get lower cased as a group.
Last updated: Dec 20 2023 at 11:08 UTC