Reals modulo period

Stream: Is there code for X?

[suhr]

Is there a type of reals quotiented by addition of period?

[Violeta Hernández]

Isn't this docs#AddCircle ?

[suhr]

I believe it is. Thanks.

[suhr]

But now I wonder if there's something like % for reals.

[suhr]

It's Int.fract for mod 1. Very confusing naming by the way.

[Yury G. Kudryashov]

See docs#toIcoMod and nearby definitions.

[Violeta Hernández]

suhr said:

It's Int.fract for mod 1. Very confusing naming by the way.

What do you find confusing? The Int namespace or the fract name?

[suhr]

Int namespace.

[Eric Wieser]

The Int is to match Int.floor which it is defined in terms of, but that's admittedly not a great reason

[Ruben Van de Velde]

It's "taking off the integer", but yeah

[Violeta Hernández]

Would anything break if we just moved this to the root namespace? It's not like we have to disambiguate, like with docs#Nat.floor and docs#Int.floor.

[Yury G. Kudryashov]

I think that we can move it, if we preserve the old names as protected deprecated aliases for those who have Int.fract in their code.

[Yury G. Kudryashov]

OTOH, a definition in the root namespace causes a minor conflict with docs#ZSpan.fract.

[Snir Broshi]

We can be trend-setters and move it to namespace Mathlib :sunglasses: