-
Notifications
You must be signed in to change notification settings - Fork 251
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: Add a DecidableEq
instance for Polynomial
#5942
Conversation
(mathlib does not compile anymore, because at some point, it needs to equate this axiom with the classically added one…) |
DecidableEq
instance for Polynomial
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
No one replied to
on Zulip, so bors merge |
Add a `DecidableEq` instance for `Polynomial` (in the presence of `DecidableEq` for coefficients). This instance is the companion of an analogue instance for `MvPolynomial`, and it allows to use if… then… else for `Polynomial` without having to `open Classical`. This also makes `Polynomial.instNormalizationMonoid` computable, by defining it in terms of this new instance. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
DecidableEq
instance for Polynomial
DecidableEq
instance for Polynomial
Add a `DecidableEq` instance for `Polynomial` (in the presence of `DecidableEq` for coefficients). This instance is the companion of an analogue instance for `MvPolynomial`, and it allows to use if… then… else for `Polynomial` without having to `open Classical`. This also makes `Polynomial.instNormalizationMonoid` computable, by defining it in terms of this new instance. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Add a `DecidableEq` instance for `Polynomial` (in the presence of `DecidableEq` for coefficients). This instance is the companion of an analogue instance for `MvPolynomial`, and it allows to use if… then… else for `Polynomial` without having to `open Classical`. This also makes `Polynomial.instNormalizationMonoid` computable, by defining it in terms of this new instance. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Add a
DecidableEq
instance forPolynomial
(in the presence ofDecidableEq
for coefficients).This instance is the companion of an analogue instance for
MvPolynomial
, and it allows to use if… then… else forPolynomial
without having toopen Classical
.This also makes
Polynomial.instNormalizationMonoid
computable, by defining it in terms of this new instance.