## 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):

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/reformulate

#### 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: May 09 2021 at 09:11 UTC