Commit 2023-12-13 23:06 5973b711

View on Github →

chore: replace piFinSuccAboveEquiv with piFinSuccAbove (#9030) Replaces Equiv.piFinSuccAboveEquiv with .piFinSuccAbove, and same for MeasurableEquiv.piFinSuccAboveEquiv

Estimated changes

Modified Mathlib/Logic/Equiv/Fin.lean

added def Equiv.piFinSuccAbove

deleted def Equiv.piFinSuccAboveEquiv

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

added theorem MeasureTheory.measurePreserving_piFinSuccAbove

deleted theorem MeasureTheory.measurePreserving_piFinSuccAboveEquiv

added theorem MeasureTheory.volume_preserving_piFinSuccAbove

deleted theorem MeasureTheory.volume_preserving_piFinSuccAboveEquiv

Modified Mathlib/MeasureTheory/Integral/Pi.lean

Modified Mathlib/MeasureTheory/Integral/TorusIntegral.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added def MeasurableEquiv.piFinSuccAbove

deleted def MeasurableEquiv.piFinSuccAboveEquiv

Modified Mathlib/RepresentationTheory/Action/Monoidal.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean