IsDiscreteValuationRing

Stream: mathlib4

[Filippo A. E. Nuccio]

In #18774 LocalRing has been (rightly) renamed to IsLocalRing, because it is Prop-valued. Given the definition of a docs#DiscreteValuationRing, I would propose that we also rename DiscreteValuationRing to IsDiscreteValuationRing. Any objection?

[Filippo A. E. Nuccio]

OK, the PR is ready #19947

[Filippo A. E. Nuccio]

I can post this in the PR reviewschannel, but perhaps here is enough.

[Kevin Buzzard]

I can't believe I called it that -- this is one of my pet hates nowadays! Yes please let's call it Is!