Even more upstreamed lemmas

YaelDillies · Feb 3, 2024 · 96051f1 · 96051f1
1 parent 077b383
commit 96051f1
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 110 deletions.
diff --git a/LeanAPAP.lean b/LeanAPAP.lean
@@ -27,7 +27,6 @@ import LeanAPAP.Mathlib.Data.Complex.Order
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Inv
 import LeanAPAP.Mathlib.Data.Finset.Card
-import LeanAPAP.Mathlib.Data.Finset.Image
 import LeanAPAP.Mathlib.Data.Fintype.Pi
 import LeanAPAP.Mathlib.Data.FunLike.Basic
 import LeanAPAP.Mathlib.Data.Nat.Parity
@@ -46,7 +45,6 @@ import LeanAPAP.Mathlib.GroupTheory.GroupAction.Defs
 import LeanAPAP.Mathlib.GroupTheory.OrderOfElement
 import LeanAPAP.Mathlib.GroupTheory.Submonoid.Basic
 import LeanAPAP.Mathlib.GroupTheory.Submonoid.Operations
-import LeanAPAP.Mathlib.Order.Partition.Finpartition
 import LeanAPAP.Mathlib.Tactic.Positivity
 import LeanAPAP.Mathlib.Tactic.Positivity.Finset
 import LeanAPAP.Physics.AlmostPeriodicity

diff --git a/LeanAPAP/Mathlib/Data/Finset/Image.lean b/LeanAPAP/Mathlib/Data/Finset/Image.lean
diff --git a/LeanAPAP/Mathlib/Data/Rat/Order.lean b/LeanAPAP/Mathlib/Data/Rat/Order.lean
@@ -1,5 +1,6 @@
 import Mathlib.Data.Rat.Order
-import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Positivity.Basic
+import Mathlib.Tactic.NormNum.Basic
 
 namespace Rat
 variable {q : ℚ}

diff --git a/LeanAPAP/Mathlib/Order/Partition/Finpartition.lean b/LeanAPAP/Mathlib/Order/Partition/Finpartition.lean