search

math-comp / algebra-tactics

Ring, field, lra, nra, and psatz tactics for Mathematical Components
33 stars 2 forks source link

Support ring expressions with exponents #11

Open pi8027 opened 3 years ago

pi8027 commented 3 years ago

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

CohenCyril commented 3 years ago

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

pi8027 commented 3 years ago

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.)

pi8027 commented 3 years ago

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?