Decimal expansion

Stream: Is there code for X?

[Yaël Dillies]

Is there some API for expansion of reals in base b? In particular, I'm interested in the period of the digits.

[Kevin Buzzard]

Wasn't someone on the discord asking about this? I remember that (for recreational maths reasons) @Calle Sönne was working on this at some point, but this was a long time ago (last summer?) The branch is digits and we made what was in retrospect a mistake of trying to work with general floor_rings and ended up being sucked into questions about when decimal expansions converged (e.g. when the floor rings have infintesimals it can get a bit complicated). I now thing that one should just develop the theory for $\R$ -- I had thought "well we want $\mathbb{Q}$ too right?" but of course one can just coerce.

[Yaël Dillies]

Yeah I remember that. And nobody made it to mathlib, right?

[Kevin Buzzard]

That was my recollection. Has there been any movement on this? I have an UG who needs them.

[Yaël Dillies]

You developed some API for LTE, right? Where is that gone?

[Yaël Dillies]

You developed some API for LTE, right? Where is that gone?

[Eric Wieser]

I had a PR for mathlib3 that I didn't both reviving