We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 0f3829e commit 193fe4eCopy full SHA for 193fe4e
1 file changed
Mathlib/Dynamics/BirkhoffSum/Maximal.lean
@@ -10,8 +10,6 @@ import Mathlib.MeasureTheory.Integral.Bochner.Set
10
import Mathlib.Algebra.Order.Group.PartialSups
11
import Mathlib.Algebra.Order.Ring.Star
12
import Mathlib.Analysis.InnerProductSpace.Basic
13
-import Mathlib.Analysis.RCLike.Lemmas
14
-import Mathlib.Data.Real.StarOrdered
15
public import Mathlib.Dynamics.BirkhoffSum.Average
16
public import Mathlib.Dynamics.BirkhoffSum.Measurable
17
public import Mathlib.Dynamics.BirkhoffSum.Integrable
0 commit comments