Name for `fractional_ideal R⁰ K`

Stream: general

[Anne Baanen]

I'm thinking the mathlib notation for fractional ideals is slightly cumbersome compared to pen-and-paper mathematics. Basically, I'd like to introduce an abbreviation along the lines of traditional_fractional_ideal R K := fractional_ideal (non_zero_divisors R) K, so we can pretend nobody needs to localize at something else than non_zero_divisors R. Ideally, I'd use fractional_ideal for what is now fractional_ideal (non_zero_divisors R) K and rename fractional ideals for other localizations to something else. (Is there a name for the more general "fractional ideals" we have in mathlib? Otherwise something like localization_ideal?)

What do you all think about this plan?

[Filippo A. E. Nuccio]

Although I understand your point of view, I have the feeling that fractional ideals wrt non-zero-divisors are prominent "only" in algebraic number theory, when studying Dedekind Domains. In general, it is common to localize at very different monoids and to consider the resulting ideals (of the form $S^{-1}I$). So I wonder if this is really worth the effort.

[Filippo A. E. Nuccio]

That being said, I'd rather called them localized_ideal.