Commit 2023-10-18 07:22 4a7ff0e3

refactor(Data/Polynomial): remove open Classical (#7706) This doesn't change any polynomial operations, but:

• Makes some Decidable values computable (otherwise, they're pointless!)
• Add a few missing arguments to lemmas here and there to make them more general This is exhaustive, within the directories it touches. Once again, the use of letI := Classical.decEq R instead of classical here is because of the weird style of proofs in these files, where if is preferred to by_cases.