Tried to find something like 'iroot'

Stream: Is there code for X?

[Ilmārs Cīrulis]

I tried to find something like "integer root" in Lean and Mathlib, but didn't have any success.

There isn't anything like that, right?

[Ilmārs Cīrulis]

That's, like, n-th root of natural number x truncated down to the closest natural number with a boolean that's true if the root is exactly a natural number (the case of x being perfect n-th power).

[Weiyi Wang]

docs#Nat.nthRoot ?
(it doesn't return whether it is exactly the root though)

[Aaron Liu]

you can test whether it's the nth root exactly by raising it to the nth power

[Ilmārs Cīrulis]

Thank you both. :heart:

[Ilmārs Cīrulis]

For some reason I didn't find it, that probably means my loogle-fu is bad.