Commit 2024-03-15 16:36 ef2b6f2b
View on Github →chore: add decidability assumptions where needed for the statement (#11157)
The general policy in mathlib is to include decidability assumptions on a theorem if and only if they are used in its statement. @fpvandoorn has been working on a linter to detect cases which violate the backwards direction of that policy. (i.e. cases where Classical.propDecidable
appears in a theorem's statement.) I've started going through the output of that linter and this PR contains fixes for the two files I've finished so far.
Zulip thread about the linter