IsDedekindDomain.HeightOneSpectrum.intValuationDef

Stream: mathlib4

[Matthew Jasper]

This definition exists so that proving that this function defines a valuation can be split into separate theorems before defining the actual valuation, but then we have some theorems about it that don't exist for intValuation. There's been some comments that we should generally be using intValuation. I'm working on a PR to minimize usage of intValuationDef. What do I do with the current intValuationDef theorems that use intValuation in their name?

• Change them to use intValuation
• Keep them and have the versions using intValuation use the same name with a '
• Something else?

[Kevin Buzzard]

I would vote for the first option. Those theorems are currently not named correctly.

[Filippo A. E. Nuccio]

Pinging @María Inés de Frutos Fernández who, I think, wrote the declaration in the first place.

[Matthew Jasper]

Also see #24644

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

I agree that the first option seems best.

[Andrew Yang]

I agree that 1 is the best. But maybe this is a good place to bring up a refactor on intValuation that I have been fond of: We should make it FractionalIdeal K -> Z instead (and specialize to elements later if necessary)