We can re-use the ring solver for expressions over ℚ, even involving inverses. The gist of it is that we can re-express any equation involving inverses to an equation between quotients of polynomials, then invoke the ring solver. Even though this idea seemed pretty dumb (surely there would be a cleverer algorithm over ℚ?), it's what the Rocq field tactic does as well. I also added some more comments explicating why ℚ is defined the way it is.
Lavenza
commented
1 month ago
We can re-use the ring solver for expressions over ℚ, even involving inverses. The gist of it is that we can re-express any equation involving inverses to an equation between quotients of polynomials, then invoke the ring solver. Even though this idea seemed pretty dumb (surely there would be a cleverer algorithm over ℚ?), it's what the Rocq
fieldtactic does as well. I also added some more comments explicating why ℚ is defined the way it is.