Commit 2024-07-31 19:18 d487a5f2

View on Github →

Chore: Remove some uses of open Classical (#15371) It is dangerous to open Classical, as it can hide that some theorem statements would be better stated with explicit decidability assumptions. This PR removes a few of them, using instead classical in proofs and open Classical in ... when needed for the statement.

Estimated changes

modified theorem MeasureTheory.measure_if
modified theorem PadicSeq.norm_equiv
modified theorem PadicSeq.norm_mul
modified theorem PadicSeq.norm_nonneg