ring tactic

Stream: new members

[Alex Zhang]

We know that tactic simp* is a variant of simp that also uses the hypotheses in the local context. Is there any analogue variant for ring that can also make use of local hypotheses?

[Kevin Buzzard]

That would be the unwritten groebner_basis tactic.

[Kevin Buzzard]

ring answers the question "Are two elements of $R[A,B,C,D,\ldots]$ equal?". What you are asking for is an answer to the question "Is the difference of these two elements of $R[A,B,C,D,\ldots]$ in this ideal?" and that's a much harder question.