Commit 2026-02-13 13:13 50648638

View on Github →

chore(Polynomial/Div): deprecate noncomputable Decidable non-instance (#34983) Deprecate decidableDvdMonic, which is a noncomputable Decidable non-instance and so inferior to Classical.dec. This is a leftover from before leanprover-community/mathlib3#1391, in which polynomials were made to use classical logic.

Estimated changes