Commit 2024-04-26 11:43 60dde2d8
View on Github →feat: add MeasurableEquiv.piOptionEquivProd (#12395) Add the def of MeasurableEquiv.piOptionEquivProd, that is the measurable equivalence for a dependent type over an Option type. This can be useful for applying induction on the product of a finite number of elements.