From 6eb43dc3bbbbf52cf197a701696070bca3bd41b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 30 Jan 2024 22:28:51 +0000 Subject: [PATCH] refactor: Delete `Algebra.GroupPower.Lemmas` (#9411) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Algebra.GroupPower.Lemmas` used to be a big bag of lemmas that made it there on the criterion that they needed "more imports". This was completely untrue, as all lemmas could be moved to earlier files in PRs: - #9440 - #9442 - #9443 - #9455 - #9456 - #9457 - #9459 - #9461 - #9463 - #9466 - #9501 - #9502 - #9503 - #9505 - #9551 - #9553 - #9720 - #9739 - #9740 - #9805 - #9806 - and this one There are several reasons for this: * Necessary lemmas have been moved to earlier files since lemmas were dumped in `Algebra.GroupPower.Lemmas` * In the Lean 3 → Lean 4 transition, Std acquired basic `Int` and `Nat` lemmas which let us shortcircuit the part of the algebraic order hierarchy on which the corresponding general lemmas rest * Some proofs were overpowered * Some earlier files were tangled and I have untangled them This PR finishes the job by moving the last few lemmas out of `Algebra.GroupPower.Lemmas`, which is therefore deleted. --- Archive/Imo/Imo2008Q3.lean | 1 - Mathlib.lean | 1 - Mathlib/Algebra/Category/GroupCat/Basic.lean | 1 - .../Algebra/EuclideanDomain/Instances.lean | 5 +- .../Algebra/GroupPower/CovariantClass.lean | 1 - Mathlib/Algebra/GroupPower/Lemmas.lean | 64 ------------------- Mathlib/Algebra/ModEq.lean | 1 - Mathlib/Algebra/Module/Basic.lean | 1 - Mathlib/Algebra/Order/Group/Lattice.lean | 1 - Mathlib/Algebra/Order/Ring/Defs.lean | 21 ++++++ Mathlib/Analysis/SpecificLimits/Basic.lean | 1 - Mathlib/Data/Int/Associated.lean | 1 - Mathlib/Data/Int/Bitwise.lean | 1 - Mathlib/Data/Nat/Pow.lean | 2 + Mathlib/Data/Real/CauSeq.lean | 2 + Mathlib/Data/Real/NNReal.lean | 1 - Mathlib/Data/ZMod/Quotient.lean | 1 - Mathlib/Dynamics/Ergodic/AddCircle.lean | 5 +- Mathlib/GroupTheory/GroupAction/Ring.lean | 2 +- Mathlib/GroupTheory/Subgroup/ZPowers.lean | 1 - Mathlib/NumberTheory/FLT/Four.lean | 1 - Mathlib/Tactic/Common.lean | 2 +- .../Topology/ContinuousFunction/Algebra.lean | 1 + Mathlib/Topology/Instances/Real.lean | 1 - 24 files changed, 32 insertions(+), 87 deletions(-) delete mode 100644 Mathlib/Algebra/GroupPower/Lemmas.lean diff --git a/Archive/Imo/Imo2008Q3.lean b/Archive/Imo/Imo2008Q3.lean index 3d2c14ae53d91..f199a524867c0 100644 --- a/Archive/Imo/Imo2008Q3.lean +++ b/Archive/Imo/Imo2008Q3.lean @@ -3,7 +3,6 @@ Copyright (c) 2021 Manuel Candales. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Manuel Candales -/ -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.Data.Real.Basic import Mathlib.Data.Real.Sqrt import Mathlib.Data.Nat.Prime diff --git a/Mathlib.lean b/Mathlib.lean index 59a0b5f36f841..b0fd5b894ef59 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -209,7 +209,6 @@ import Mathlib.Algebra.GroupPower.CovariantClass import Mathlib.Algebra.GroupPower.Hom import Mathlib.Algebra.GroupPower.Identities import Mathlib.Algebra.GroupPower.IterateHom -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.Algebra.GroupPower.NegOnePow import Mathlib.Algebra.GroupPower.Order import Mathlib.Algebra.GroupPower.Ring diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean index 7b9c0e6acaad2..d06ad3d2273c7 100644 --- a/Mathlib/Algebra/Category/GroupCat/Basic.lean +++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin -/ import Mathlib.Algebra.Category.MonCat.Basic -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.CategoryTheory.Endomorphism #align_import algebra.category.Group.basic from "leanprover-community/mathlib"@"524793de15bc4c52ee32d254e7d7867c7176b3af" diff --git a/Mathlib/Algebra/EuclideanDomain/Instances.lean b/Mathlib/Algebra/EuclideanDomain/Instances.lean index a9ae72c47a1a4..b3902b78cf46e 100644 --- a/Mathlib/Algebra/EuclideanDomain/Instances.lean +++ b/Mathlib/Algebra/EuclideanDomain/Instances.lean @@ -6,11 +6,8 @@ Authors: Louis Carlin, Mario Carneiro import Mathlib.Algebra.EuclideanDomain.Defs import Mathlib.Algebra.Field.Defs import Mathlib.Algebra.GroupWithZero.Units.Lemmas -import Mathlib.Algebra.Order.Ring.Lemmas -import Mathlib.Init.Data.Int.Order -import Mathlib.Data.Int.Basic -import Mathlib.Data.Nat.Order.Basic import Mathlib.Data.Int.Order.Basic +import Mathlib.Data.Nat.Order.Basic #align_import algebra.euclidean_domain.instances from "leanprover-community/mathlib"@"e1bccd6e40ae78370f01659715d3c948716e3b7e" diff --git a/Mathlib/Algebra/GroupPower/CovariantClass.lean b/Mathlib/Algebra/GroupPower/CovariantClass.lean index 418c3b742928f..d0b39bea61e71 100644 --- a/Mathlib/Algebra/GroupPower/CovariantClass.lean +++ b/Mathlib/Algebra/GroupPower/CovariantClass.lean @@ -5,7 +5,6 @@ Authors: Jeremy Avigad, Robert Y. Lewis, Yury G. Kudryashov -/ import Mathlib.Algebra.GroupPower.Basic import Mathlib.Algebra.Order.Monoid.OrderDual -import Mathlib.Data.Nat.Defs import Mathlib.Tactic.Monotonicity.Attr /-! diff --git a/Mathlib/Algebra/GroupPower/Lemmas.lean b/Mathlib/Algebra/GroupPower/Lemmas.lean deleted file mode 100644 index 5ff1c89a6feb8..0000000000000 --- a/Mathlib/Algebra/GroupPower/Lemmas.lean +++ /dev/null @@ -1,64 +0,0 @@ -/- -Copyright (c) 2015 Jeremy Avigad. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jeremy Avigad, Robert Y. Lewis --/ -import Mathlib.Data.Nat.Order.Basic - -#align_import algebra.group_power.lemmas from "leanprover-community/mathlib"@"a07d750983b94c530ab69a726862c2ab6802b38c" - -/-! -# Lemmas about power operations on monoids and groups - -This file contains lemmas about `Monoid.pow`, `Group.pow`, `nsmul`, and `zsmul` -which require additional imports besides those available in `Mathlib.Algebra.GroupPower.Basic`. --/ - -open Int - -universe u v w x y z u₁ u₂ - -variable {α : Type*} {M : Type u} {N : Type v} {G : Type w} {H : Type x} {A : Type y} {B : Type z} - {R : Type u₁} {S : Type u₂} - -section OrderedSemiring - -variable [OrderedSemiring R] {a : R} - -theorem pow_le_pow_of_le_one_aux (h : 0 ≤ a) (ha : a ≤ 1) (i : ℕ) : - ∀ k : ℕ, a ^ (i + k) ≤ a ^ i - | 0 => by simp - | k + 1 => by - rw [← add_assoc, ← one_mul (a ^ i), pow_succ] - exact mul_le_mul ha (pow_le_pow_of_le_one_aux h ha _ _) (pow_nonneg h _) zero_le_one --- Porting note: no #align because private in Lean 3 - -theorem pow_le_pow_of_le_one (h : 0 ≤ a) (ha : a ≤ 1) {i j : ℕ} (hij : i ≤ j) : a ^ j ≤ a ^ i := by - let ⟨k, hk⟩ := Nat.exists_eq_add_of_le hij - rw [hk]; exact pow_le_pow_of_le_one_aux h ha _ _ -#align pow_le_pow_of_le_one pow_le_pow_of_le_one - -theorem pow_le_of_le_one (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ a := - (pow_one a).subst (pow_le_pow_of_le_one h₀ h₁ (Nat.pos_of_ne_zero hn)) -#align pow_le_of_le_one pow_le_of_le_one - -theorem sq_le (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a := - pow_le_of_le_one h₀ h₁ two_ne_zero -#align sq_le sq_le - -end OrderedSemiring - -section LinearOrderedSemiring - -variable [LinearOrderedSemiring R] - -theorem sign_cases_of_C_mul_pow_nonneg {C r : R} (h : ∀ n : ℕ, 0 ≤ C * r ^ n) : - C = 0 ∨ 0 < C ∧ 0 ≤ r := by - have : 0 ≤ C := by simpa only [pow_zero, mul_one] using h 0 - refine' this.eq_or_lt.elim (fun h => Or.inl h.symm) fun hC => Or.inr ⟨hC, _⟩ - refine' nonneg_of_mul_nonneg_right _ hC - simpa only [pow_one] using h 1 -set_option linter.uppercaseLean3 false in -#align sign_cases_of_C_mul_pow_nonneg sign_cases_of_C_mul_pow_nonneg - -end LinearOrderedSemiring diff --git a/Mathlib/Algebra/ModEq.lean b/Mathlib/Algebra/ModEq.lean index 1759fda7373d5..c9f343eca3317 100644 --- a/Mathlib/Algebra/ModEq.lean +++ b/Mathlib/Algebra/ModEq.lean @@ -3,7 +3,6 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.Data.Int.ModEq import Mathlib.GroupTheory.QuotientGroup diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean index b3a040efd54e0..f3726ece3e759 100644 --- a/Mathlib/Algebra/Module/Basic.lean +++ b/Mathlib/Algebra/Module/Basic.lean @@ -3,7 +3,6 @@ Copyright (c) 2015 Nathaniel Thomas. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro -/ -import Mathlib.Algebra.Field.Defs import Mathlib.Algebra.Function.Indicator import Mathlib.Algebra.SMulWithZero import Mathlib.GroupTheory.GroupAction.Group diff --git a/Mathlib/Algebra/Order/Group/Lattice.lean b/Mathlib/Algebra/Order/Group/Lattice.lean index 12a0d2f3fdb4c..0154e658cd5f0 100644 --- a/Mathlib/Algebra/Order/Group/Lattice.lean +++ b/Mathlib/Algebra/Order/Group/Lattice.lean @@ -3,7 +3,6 @@ Copyright (c) 2021 Christopher Hoskin. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Christopher Hoskin, Yaël Dillies -/ -import Mathlib.Algebra.GroupPower.Basic import Mathlib.Algebra.Order.Group.OrderIso #align_import algebra.order.lattice_group from "leanprover-community/mathlib"@"5dc275ec639221ca4d5f56938eb966f6ad9bc89f" diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean index f3ac783c1d4ed..9ee5dec9da8ce 100644 --- a/Mathlib/Algebra/Order/Ring/Defs.lean +++ b/Mathlib/Algebra/Order/Ring/Defs.lean @@ -250,6 +250,20 @@ theorem pow_nonneg (H : 0 ≤ a) : ∀ n : ℕ, 0 ≤ a ^ n exact mul_nonneg H (pow_nonneg H _) #align pow_nonneg pow_nonneg +lemma pow_le_pow_of_le_one (ha₀ : 0 ≤ a) (ha₁ : a ≤ 1) : ∀ {m n : ℕ}, m ≤ n → a ^ n ≤ a ^ m + | _, _, Nat.le.refl => le_rfl + | _, _, Nat.le.step h => by + rw [pow_succ] + exact (mul_le_of_le_one_left (pow_nonneg ha₀ _) ha₁).trans $ pow_le_pow_of_le_one ha₀ ha₁ h +#align pow_le_pow_of_le_one pow_le_pow_of_le_one + +lemma pow_le_of_le_one (h₀ : 0 ≤ a) (h₁ : a ≤ 1) {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ a := + (pow_one a).subst (pow_le_pow_of_le_one h₀ h₁ (Nat.pos_of_ne_zero hn)) +#align pow_le_of_le_one pow_le_of_le_one + +lemma sq_le (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a := pow_le_of_le_one h₀ h₁ two_ne_zero +#align sq_le sq_le + -- Porting note: it's unfortunate we need to write `(@one_le_two α)` here. theorem add_le_mul_two_add (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) := calc @@ -1048,6 +1062,13 @@ theorem mul_self_inj {a b : α} (h1 : 0 ≤ a) (h2 : 0 ≤ b) : a * a = b * b (@strictMonoOn_mul_self α _).eq_iff_eq h1 h2 #align mul_self_inj mul_self_inj +lemma sign_cases_of_C_mul_pow_nonneg (h : ∀ n, 0 ≤ a * b ^ n) : a = 0 ∨ 0 < a ∧ 0 ≤ b := by + have : 0 ≤ a := by simpa only [pow_zero, mul_one] using h 0 + refine this.eq_or_gt.imp_right fun ha ↦ ⟨ha, nonneg_of_mul_nonneg_right ?_ ha⟩ + simpa only [pow_one] using h 1 +set_option linter.uppercaseLean3 false in +#align sign_cases_of_C_mul_pow_nonneg sign_cases_of_C_mul_pow_nonneg + variable [ExistsAddOfLE α] -- See note [lower instance priority] diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index fd8f02ceb43ae..6669022b25d8b 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sébastien Gouëzel, Johannes Hölzl, Yury G. Kudryashov, Patrick Massot -/ import Mathlib.Algebra.GeomSum -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.Order.Filter.Archimedean import Mathlib.Order.Iterate import Mathlib.Topology.Instances.ENNReal diff --git a/Mathlib/Data/Int/Associated.lean b/Mathlib/Data/Int/Associated.lean index 0a94531cc8ce7..f56847e046af1 100644 --- a/Mathlib/Data/Int/Associated.lean +++ b/Mathlib/Data/Int/Associated.lean @@ -5,7 +5,6 @@ Authors: Anne Baanen -/ import Mathlib.Algebra.Associated import Mathlib.Data.Int.Units -import Mathlib.Data.Int.Basic #align_import data.int.associated from "leanprover-community/mathlib"@"207cfac9fcd06138865b5d04f7091e46d9320432" /-! diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index 9ddfb504c328c..92ee8887ee721 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -5,7 +5,6 @@ Authors: Jeremy Avigad -/ import Mathlib.Data.Int.Basic import Mathlib.Data.Nat.Bitwise -import Mathlib.Data.Nat.Pow import Mathlib.Data.Nat.Size import Mathlib.Init.Data.Int.Bitwise diff --git a/Mathlib/Data/Nat/Pow.lean b/Mathlib/Data/Nat/Pow.lean index dc50206a8ab5b..bde1e4b6efe99 100644 --- a/Mathlib/Data/Nat/Pow.lean +++ b/Mathlib/Data/Nat/Pow.lean @@ -241,3 +241,5 @@ Those lemmas have been deprecated on 2023-12-23. @[deprecated] protected alias Nat.pow_right_strictMono := pow_right_strictMono @[deprecated] alias Nat.pow_le_iff_le_right := pow_le_pow_iff_right @[deprecated] alias Nat.pow_lt_iff_lt_right := pow_lt_pow_iff_right + +assert_not_exists Set.range diff --git a/Mathlib/Data/Real/CauSeq.lean b/Mathlib/Data/Real/CauSeq.lean index da1924bc15e09..0be28f2058d4a 100644 --- a/Mathlib/Data/Real/CauSeq.lean +++ b/Mathlib/Data/Real/CauSeq.lean @@ -1001,3 +1001,5 @@ protected theorem sup_inf_distrib_right (a b c : CauSeq α abs) : a ⊓ b ⊔ c end Abs end CauSeq + +assert_not_exists Module diff --git a/Mathlib/Data/Real/NNReal.lean b/Mathlib/Data/Real/NNReal.lean index e5d9c96b7632a..7a113ac54235e 100644 --- a/Mathlib/Data/Real/NNReal.lean +++ b/Mathlib/Data/Real/NNReal.lean @@ -6,7 +6,6 @@ Authors: Johan Commelin import Mathlib.Algebra.Algebra.Basic import Mathlib.Algebra.BigOperators.Order import Mathlib.Algebra.BigOperators.Ring -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.Algebra.Order.Field.Canonical.Basic import Mathlib.Algebra.Order.Nonneg.Field import Mathlib.Algebra.Order.Nonneg.Floor diff --git a/Mathlib/Data/ZMod/Quotient.lean b/Mathlib/Data/ZMod/Quotient.lean index 482e34b05aed8..8ada52d6a4846 100644 --- a/Mathlib/Data/ZMod/Quotient.lean +++ b/Mathlib/Data/ZMod/Quotient.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Anne Baanen -/ import Mathlib.Algebra.Group.Equiv.TypeTags -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.Data.ZMod.Basic import Mathlib.GroupTheory.GroupAction.Quotient import Mathlib.RingTheory.Ideal.QuotientOperations diff --git a/Mathlib/Dynamics/Ergodic/AddCircle.lean b/Mathlib/Dynamics/Ergodic/AddCircle.lean index 0ef7ce731fc63..0113f4262fc97 100644 --- a/Mathlib/Dynamics/Ergodic/AddCircle.lean +++ b/Mathlib/Dynamics/Ergodic/AddCircle.lean @@ -3,10 +3,11 @@ Copyright (c) 2022 Oliver Nash. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Oliver Nash -/ -import Mathlib.MeasureTheory.Group.AddCircle +import Mathlib.Algebra.Order.Ring.Abs +import Mathlib.Data.Set.Pointwise.Iterate import Mathlib.Dynamics.Ergodic.Ergodic import Mathlib.MeasureTheory.Covering.DensityTheorem -import Mathlib.Data.Set.Pointwise.Iterate +import Mathlib.MeasureTheory.Group.AddCircle import Mathlib.MeasureTheory.Measure.Haar.Unique #align_import dynamics.ergodic.add_circle from "leanprover-community/mathlib"@"5f6e827d81dfbeb6151d7016586ceeb0099b9655" diff --git a/Mathlib/GroupTheory/GroupAction/Ring.lean b/Mathlib/GroupTheory/GroupAction/Ring.lean index c99e4cf635df7..2b02a7b187389 100644 --- a/Mathlib/GroupTheory/GroupAction/Ring.lean +++ b/Mathlib/GroupTheory/GroupAction/Ring.lean @@ -39,7 +39,7 @@ instance NonUnitalNonAssocSemiring.nat_isScalarTower [NonUnitalNonAssocSemiring · simp_rw [succ_nsmul, ← ih, smul_eq_mul, add_mul] #align non_unital_non_assoc_semiring.nat_is_scalar_tower NonUnitalNonAssocSemiring.nat_isScalarTower -/-- Note that `AddGroup.int_smulCommClass` requires stronger assumptions on `α`. -/ +/-- Note that `AddMonoid.int_smulCommClass` requires stronger assumptions on `α`. -/ instance NonUnitalNonAssocRing.int_smulCommClass [NonUnitalNonAssocRing α] : SMulCommClass ℤ α α where smul_comm n x y := diff --git a/Mathlib/GroupTheory/Subgroup/ZPowers.lean b/Mathlib/GroupTheory/Subgroup/ZPowers.lean index d9fb32558be73..99a2015fc5c3b 100644 --- a/Mathlib/GroupTheory/Subgroup/ZPowers.lean +++ b/Mathlib/GroupTheory/Subgroup/ZPowers.lean @@ -3,7 +3,6 @@ Copyright (c) 2020 Chris Hughes. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Chris Hughes -/ -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.GroupTheory.Subgroup.Basic import Mathlib.Data.Countable.Basic import Mathlib.Data.Set.Image diff --git a/Mathlib/NumberTheory/FLT/Four.lean b/Mathlib/NumberTheory/FLT/Four.lean index e56e2937c3935..6d7723ec6966f 100644 --- a/Mathlib/NumberTheory/FLT/Four.lean +++ b/Mathlib/NumberTheory/FLT/Four.lean @@ -3,7 +3,6 @@ Copyright (c) 2020 Paul van Wamelen. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Paul van Wamelen -/ -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.NumberTheory.FLT.Basic import Mathlib.NumberTheory.PythagoreanTriples import Mathlib.RingTheory.Coprime.Lemmas diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index 407ac154b9d34..6a9ceee4a8604 100644 --- a/Mathlib/Tactic/Common.lean +++ b/Mathlib/Tactic/Common.lean @@ -58,7 +58,7 @@ import Mathlib.Tactic.LibrarySearch import Mathlib.Tactic.Lift import Mathlib.Tactic.Lint import Mathlib.Tactic.MkIffOfInductiveProp --- NormNum imports `Mathlib.Algebra.GroupPower.Lemmas` and `Mathlib.Algebra.Order.Invertible` +-- NormNum imports `Algebra.Order.Invertible`, `Data.Int.Basic`, `Data.Nat.Cast.Commute` -- import Mathlib.Tactic.NormNum.Basic import Mathlib.Tactic.NthRewrite import Mathlib.Tactic.Observe diff --git a/Mathlib/Topology/ContinuousFunction/Algebra.lean b/Mathlib/Topology/ContinuousFunction/Algebra.lean index ffee7b0f194d7..432984a70ad18 100644 --- a/Mathlib/Topology/ContinuousFunction/Algebra.lean +++ b/Mathlib/Topology/ContinuousFunction/Algebra.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Scott Morrison, Nicolò Cavalleri -/ import Mathlib.Algebra.Algebra.Pi +import Mathlib.Algebra.Order.Group.Lattice import Mathlib.Algebra.Periodic import Mathlib.Algebra.Algebra.Subalgebra.Basic import Mathlib.Algebra.Star.StarAlgHom diff --git a/Mathlib/Topology/Instances/Real.lean b/Mathlib/Topology/Instances/Real.lean index 9658c74c5c1cb..90b9e48892b4f 100644 --- a/Mathlib/Topology/Instances/Real.lean +++ b/Mathlib/Topology/Instances/Real.lean @@ -3,7 +3,6 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Mario Carneiro -/ -import Mathlib.Algebra.GroupPower.Lemmas import Mathlib.Algebra.Periodic import Mathlib.Topology.Algebra.UniformMulAction import Mathlib.Topology.Algebra.Star