field_simp'?

Stream: Is there code for X?

[Alex Kontorovich]

From offline discussion: could there be a field_simp', with the following behavior: when it sees that the goal has denominators, but doesn't know that they're nonzero, rather than manipulating the goal directly (or just failing), it could generate a hypothesis that, if the denominators could be proved nonzero, then this is what the expression would turn into, with everything cross-multiplied...?

[Alex Kontorovich]

By the way, this is basically what algebraic manipulation in computer algebra systems does, right? It just assumes every denominator is non-zero and cross-multiplies. Of course we can't do that, but maybe we can auto-generate the requisite hypotheses that would allow it. (This would also help someone trying to figure out why field_simp isn't resolving things...)

[Ruben Van de Velde]

Yeah, this has been discussed before, but I don't think anyone has volunteered to work on it