Support ring expressions with exponents

Open pi8027 opened this issue 4 years ago • 3 comments

I have no idea how to do this normalization by reflection though.

Sep 22 '21 09:09 pi8027

Isn't it a matter of reading the Table 1 as reduction rules on the exponents?

Sep 22 '21 09:09 CohenCyril

When I put some thought into this, I didn't think so. But now I don't remember the details. Let me do that later. (Now I'm just making my TODOs explicit by putting them as issues.)

Sep 22 '21 09:09 pi8027

BTW, Lean's ring_exp tactic does not seem to solve (a * b + a * c) ^ n = a ^ n * (b + c) ^ n (not tested). Is there something we can do with such cases?

Sep 27 '21 13:09 pi8027