Commit 2023-11-07 17:41 a051ac5f

feat: improve polyrith by testing for membership in the radical (#7790) In @hrmacbeth 's tutorial on polyrith, there were examples of problems that it could almost solve, but failed. The goal was not expressible as a linear combination of the hypotheses but a power of the goal was.

example (x y z : ℚ) (h : x = y) (h2 : x * y = 0) : x + y*z = 0 :=
sorry

Mathematically, x+y*z is in the radical of the ideal generated by x-y, x*y. There's a "standard trick" for testing membership in the radical without a search for the proper exponent: see e.g. section 2.2 of arxiv.org/pdf/1007.3615.pdf or 4.2 Prop 8 of Cox, Little, O'Shea. This PR implements the trick in the Sage call made by polyrith. When the power returned is n > 1, we use linear_combination (exp := n) to check the certificate (#7789 ). The polyrith test infrastructure still needs to be ported from mathlib3. All tests in the test file succeed when they are uncommented. A future PR will restore the old test suite.