Commit 2024-03-15 16:36 ef2b6f2b

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