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.