We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 4c626f3 commit aaf8272Copy full SHA for aaf8272
1 file changed
Mathlib.lean
@@ -4389,7 +4389,9 @@ public import Mathlib.Data.ZMod.ValMinAbs
4389
public import Mathlib.Deprecated.Aliases
4390
public import Mathlib.Dynamics.BirkhoffSum.Average
4391
public import Mathlib.Dynamics.BirkhoffSum.Basic
4392
+public import Mathlib.Dynamics.BirkhoffSum.Integrable
4393
public import Mathlib.Dynamics.BirkhoffSum.Maximal
4394
+public import Mathlib.Dynamics.BirkhoffSum.Measurable
4395
public import Mathlib.Dynamics.BirkhoffSum.NormedSpace
4396
public import Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
4397
public import Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
0 commit comments