ring_exp ?

Stream: mathlib4

[Michael Stoll]

Does ring_exp exist in Mathlib4? Currently, it gives me "unknown tactic".

[Yury G. Kudryashov]

No, could you post an #mwe that needs it (i.e., ring fails but mathlib3 ring_exp works)?

[Michael Stoll]

I was trying to use it in some situation where I thought it might work, but thinking again, I don't think I should expect that it would. (It would need to know that 4 ^ n = 2 ^ (2 * n) or similar.)

[Michael Stoll]

So the claim is that Mathlib4 ring does everything mathlib3 ring_exp did?

[Yury G. Kudryashov]

I don't know.

[Mario Carneiro]

lean 4 ring is lean 3 ring_exp