Commit 2022-07-12 03:56 423a8b92
View on Github →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.