three dedekind domains

Stream: mathlib4

[Aaron Liu]

We have a typeclass that expresses the fact that a commutative ring is a dedekind domain, docs#IsDedekindDomain.
We also have another typeclass that does the same thing, but does not bundle the IsDomain hypothesis, docs#IsDedekindDomainDvr.
And we also have docs#IsDedekindDomainInv, which is the same as IsDedekindDomainDvr, except it's not a typeclass.

They are all equivalent, witnessed by docs#IsDedekindDomain.isDedekindDomainDvr, docs#IsDedekindDomainDvr.isDedekindDomain, docs#isDedkindDomain_iff_isDedekindDomainInv. It seems to me that docs#IsDedekindDomain is the "canonical" one. Should we do something about the other two? I don't think we want three of the same thing in mathlib.

[Yaël Dillies]

IsDe...Inv is an auxiliary typeclass. If you manage to make it private, please open a PR and I'll approve it

[Yaël Dillies]

I don't know about IsDe...Dvr

[María Inés de Frutos Fernández]

@Anne Baanen, @Sander Dahmen, @Ashvni Narayanan, @Filippo A. E. Nuccio

[Anne Baanen]

Both are auxiliary typeclasses, and refactors turning them into (non-public ∨ non-classes) are welcome. (Although, please make sure it's still easy to go between the statement using FractionRing and an arbitrary K that satisfies IsFractionRing.)

[Filippo A. E. Nuccio]

Why also "non-classes" ? Wouldn't "non-public" suffice?

[Anne Baanen]

Ah sorry, I meant to put an or in between :)

[Filippo A. E. Nuccio]

Ah, then I certainly agree with your point!