Zulip Chat Archive
Stream: mathlib4
Topic: tfae naming
Ruben Van de Velde (Mar 17 2023 at 15:31):
What should tfae theorems be called? We have IsLocallyConstant.tfae, noetherianSpace_TFAE and IsEquiv_tFAE
Ruben Van de Velde (Mar 17 2023 at 15:32):
(I'm thinking not the last one)
Mario Carneiro (Mar 17 2023 at 15:33):
I think the usual naming rule works well enough here. TFAE is the type name, and tfae is used when it is a theorem label segment
Matthew Ballard (Mar 17 2023 at 15:33):
isEquiv_tfae?
Matthew Ballard (Mar 17 2023 at 15:33):
As Mario said, if it is a theorem
Mario Carneiro (Mar 17 2023 at 15:34):
(this is covered by the rule for lowercasing the initial capital cluster as a group)
Last updated: Dec 20 2023 at 11:08 UTC