Zulip Chat Archive
Stream: maths
Topic: equivalent definitions
Johan Commelin (Sep 01 2020 at 08:20):
Continuing discussion from here:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60prop_limits.60.20branch/near/208657290
@Damiano Testa would like to have a method to "jump" between equivalent definitions.
I wonder if we can do something to make this easier. We'll be getting more and more of those over time.
Johan Commelin (Sep 01 2020 at 08:20):
We already have this for local_ring, discrete_valuation_ring and there is a PR with three definitions of Dedekind domain.
Johan Commelin (Sep 01 2020 at 08:21):
Yury has proven some tfae lemmas in analysis. But I'm not sure that is the best way. (Maybe it is!)
Johan Commelin (Sep 01 2020 at 08:21):
Should we have an attribute @[alt_def name_of.main_def]
Patrick Massot (Sep 01 2020 at 08:47):
Johan Commelin (Sep 01 2020 at 08:51):
@Patrick Massot Yes, reformulate is a good idea. But maybe a "curated" approach could give even better results?
Johan Commelin (Sep 01 2020 at 08:52):
I do think that reformulate is "low-hanging" fruit for our community (not for me!). So we should probably try that first.
Patrick Massot (Sep 01 2020 at 09:10):
What do you mean by curated? You want a new attribute? I'd like to try the automated approach first. It seems very low hanging indeed, but you still need someone taking some time to do it.
Johan Commelin (Sep 01 2020 at 09:11):
With "curated" I indeed was thinking of a new attribute, as I suggested above.
Last updated: Dec 20 2023 at 11:08 UTC