mathlib

423a8b92 - feat(tactic/polyrith): a tactic using Sage to solve polynomial equalities with hypotheses (#14878)

feat(tactic/polyrith): a tactic using Sage to solve polynomial equalities with hypotheses (#14878) Created a new tactic called polyrith that solves polynomial equalities through polynomial arithmetic on the hypotheses/proof terms. Similar to how linarith solves linear equalities through linear arithmetic on the hypotheses/proof terms. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>