Commit 2025-04-21 11:48 a76a6a39

View on Github →

chore(Probability/Distributions): remove open Classical ... from toMeasure_uniformOfFintype_apply (#24074) Remove open scoped Classical in in front of the toOuterMeasure_uniformOfFintype_apply and toMeasure_uniformOfFintype_apply theorems

Estimated changes

Modified Mathlib/Probability/Distributions/Uniform.lean

modified theorem PMF.toMeasure_uniformOfFintype_apply

modified theorem PMF.toOuterMeasure_uniformOfFintype_apply