bump to nightly-2024-04-07-08

mathlib commit leanprover-community/mathlib@65a1391
leanprover-community · Apr 7, 2024 · b03b865 · b03b865
1 parent e34029c
commit b03b865
Show file tree

Hide file tree

Showing 162 changed files with 321 additions and 405 deletions.
diff --git a/Archive/Imo/Imo1994Q1.lean b/Archive/Imo/Imo1994Q1.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Labelle
 -/
 import Algebra.BigOperators.Basic
-import Algebra.BigOperators.Order
+import Algebra.Order.BigOperators.Group.Finset
 import Data.Fintype.BigOperators
 import Data.Finset.Sort
 import Data.Fin.Interval

diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean
@@ -5,7 +5,7 @@ Authors: Oliver Nash
 -/
 import Data.Fintype.Prod
 import Data.Int.Parity
-import Algebra.BigOperators.Order
+import Algebra.Order.BigOperators.Group.Finset
 import Tactic.Ring
 import Tactic.NoncommRing
 

diff --git a/Archive/Imo/Imo2006Q5.lean b/Archive/Imo/Imo2006Q5.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Violeta Hernández Palacios. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Violeta Hernández Palacios
 -/
-import Data.Polynomial.RingDivision
+import Algebra.Polynomial.RingDivision
 import Dynamics.PeriodicPts
 
 #align_import imo.imo2006_q5 from "leanprover-community/mathlib"@"08b081ea92d80e3a41f899eea36ef6d56e0f1db0"

diff --git a/Archive/Imo/Imo2019Q4.lean b/Archive/Imo/Imo2019Q4.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import Tactic.IntervalCases
-import Algebra.BigOperators.Order
+import Algebra.Order.BigOperators.Group.Finset
 import Data.Nat.Multiplicity
 
 #align_import imo.imo2019_q4 from "leanprover-community/mathlib"@"08b081ea92d80e3a41f899eea36ef6d56e0f1db0"

diff --git a/Archive/OxfordInvariants/2021summer/Week3P1.lean b/Archive/OxfordInvariants/2021summer/Week3P1.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
-import Algebra.BigOperators.Order
+import Algebra.Order.BigOperators.Group.Finset
 import Algebra.BigOperators.Ring
 import Algebra.CharZero.Lemmas
 import Data.Rat.Cast.Defs

diff --git a/Counterexamples/MapFloor.lean b/Counterexamples/MapFloor.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Algebra.Order.Hom.Ring
-import Data.Polynomial.Reverse
+import Algebra.Polynomial.Reverse
 
 #align_import map_floor from "leanprover-community/mathlib"@"08b081ea92d80e3a41f899eea36ef6d56e0f1db0"
 

diff --git a/Mathbin/Algebra/AlgebraicCard.lean b/Mathbin/Algebra/AlgebraicCard.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Violeta Hernández Palacios. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Violeta Hernández Palacios
 -/
-import Data.Polynomial.Cardinal
+import Algebra.Polynomial.Cardinal
 import RingTheory.Algebraic
 
 #align_import algebra.algebraic_card from "leanprover-community/mathlib"@"38df578a6450a8c5142b3727e3ae894c2300cae0"

diff --git a/Mathbin/Algebra/BigOperators/Basic.lean b/Mathbin/Algebra/BigOperators/Basic.lean
@@ -172,7 +172,7 @@ protected theorem map_prod [CommMonoid β] [CommMonoid γ] (g : β →* γ) (f :
     g (∏ x in s, f x) = ∏ x in s, g (f x) :=
   map_prod g f s
 #align monoid_hom.map_prod map_prodₓ
-#align add_monoid_hom.map_sum map_sumₓ
+#align linear_map.map_sum map_sumₓ
 
 /- warning: mul_equiv.map_prod clashes with monoid_hom.map_prod -> map_prodₓ
 Case conversion may be inaccurate. Consider using '#align mul_equiv.map_prod map_prodₓₓ'. -/
@@ -183,7 +183,7 @@ protected theorem map_prod [CommMonoid β] [CommMonoid γ] (g : β ≃* γ) (f :
     g (∏ x in s, f x) = ∏ x in s, g (f x) :=
   map_prod g f s
 #align mul_equiv.map_prod map_prodₓ
-#align add_monoid_hom.map_sum map_sumₓ
+#align linear_map.map_sum map_sumₓ
 -/
 
 #print RingHom.map_list_prod /-

diff --git a/Mathbin/Algebra/BigOperators/Finprod.lean b/Mathbin/Algebra/BigOperators/Finprod.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Kexing Ying and Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying, Kevin Buzzard, Yury Kudryashov
 -/
-import Algebra.BigOperators.Order
+import Algebra.Order.BigOperators.Group.Finset
 import Algebra.Function.Indicator
 
 #align_import algebra.big_operators.finprod from "leanprover-community/mathlib"@"63f84d91dd847f50bae04a01071f3a5491934e36"

diff --git a/Mathbin/Algebra/BigOperators/Finsupp.lean b/Mathbin/Algebra/BigOperators/Finsupp.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau
 import Data.Finsupp.Indicator
 import Algebra.BigOperators.Pi
 import Algebra.BigOperators.Ring
-import Algebra.BigOperators.Order
+import Algebra.Order.BigOperators.Group.Finset
 import GroupTheory.Submonoid.Membership
 
 #align_import algebra.big_operators.finsupp from "leanprover-community/mathlib"@"842328d9df7e96fd90fc424e115679c15fb23a71"

diff --git a/Mathbin/Algebra/Category/Ring/Adjunctions.lean b/Mathbin/Algebra/Category/Ring/Adjunctions.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Johannes Hölzl
 -/
 import Algebra.Category.Ring.Basic
-import Data.MvPolynomial.CommRing
+import Algebra.MvPolynomial.CommRing
 
 #align_import algebra.category.Ring.adjunctions from "leanprover-community/mathlib"@"f60c6087a7275b72d5db3c5a1d0e19e35a429c0a"
 

diff --git a/Mathbin/Algebra/CubicDiscriminant.lean b/Mathbin/Algebra/CubicDiscriminant.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 David Kurniadi Angdinata. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Kurniadi Angdinata
 -/
-import Data.Polynomial.Splits
+import Algebra.Polynomial.Splits
 
 #align_import algebra.cubic_discriminant from "leanprover-community/mathlib"@"31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0"
 

diff --git a/Mathbin/Algebra/Field/Basic.lean b/Mathbin/Algebra/Field/Basic.lean
@@ -352,22 +352,22 @@ section NoncomputableDefs
 
 variable {R : Type _} [Nontrivial R]
 
-#print divisionRingOfIsUnitOrEqZero /-
+#print DivisionRing.ofIsUnitOrEqZero /-
 /-- Constructs a `division_ring` structure on a `ring` consisting only of units and 0. -/
-noncomputable def divisionRingOfIsUnitOrEqZero [hR : Ring R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
+noncomputable def DivisionRing.ofIsUnitOrEqZero [hR : Ring R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
     DivisionRing R :=
   { groupWithZeroOfIsUnitOrEqZero h, hR with }
-#align division_ring_of_is_unit_or_eq_zero divisionRingOfIsUnitOrEqZero
+#align division_ring_of_is_unit_or_eq_zero DivisionRing.ofIsUnitOrEqZero
 -/
 
-#print fieldOfIsUnitOrEqZero /-
+#print Field.ofIsUnitOrEqZero /-
 /-- Constructs a `field` structure on a `comm_ring` consisting only of units and 0.
 See note [reducible non-instances]. -/
 @[reducible]
-noncomputable def fieldOfIsUnitOrEqZero [hR : CommRing R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
+noncomputable def Field.ofIsUnitOrEqZero [hR : CommRing R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
     Field R :=
   { groupWithZeroOfIsUnitOrEqZero h, hR with }
-#align field_of_is_unit_or_eq_zero fieldOfIsUnitOrEqZero
+#align field_of_is_unit_or_eq_zero Field.ofIsUnitOrEqZero
 -/
 
 end NoncomputableDefs
@@ -477,18 +477,18 @@ instance [h : Semifield α] : Semifield αᵒᵈ :=
 instance [h : Field α] : Field αᵒᵈ :=
   h
 
-#print toDual_rat_cast /-
+#print toDual_ratCast /-
 @[simp]
-theorem toDual_rat_cast [HasRatCast α] (n : ℚ) : toDual (n : α) = n :=
+theorem toDual_ratCast [HasRatCast α] (n : ℚ) : toDual (n : α) = n :=
   rfl
-#align to_dual_rat_cast toDual_rat_cast
+#align to_dual_rat_cast toDual_ratCast
 -/
 
-#print ofDual_rat_cast /-
+#print ofDual_ratCast /-
 @[simp]
-theorem ofDual_rat_cast [HasRatCast α] (n : ℚ) : (ofDual n : α) = n :=
+theorem ofDual_ratCast [HasRatCast α] (n : ℚ) : (ofDual n : α) = n :=
   rfl
-#align of_dual_rat_cast ofDual_rat_cast
+#align of_dual_rat_cast ofDual_ratCast
 -/
 
 /-! ### Lexicographic order -/
@@ -509,17 +509,17 @@ instance [h : Semifield α] : Semifield (Lex α) :=
 instance [h : Field α] : Field (Lex α) :=
   h
 
-#print toLex_rat_cast /-
+#print toLex_ratCast /-
 @[simp]
-theorem toLex_rat_cast [HasRatCast α] (n : ℚ) : toLex (n : α) = n :=
+theorem toLex_ratCast [HasRatCast α] (n : ℚ) : toLex (n : α) = n :=
   rfl
-#align to_lex_rat_cast toLex_rat_cast
+#align to_lex_rat_cast toLex_ratCast
 -/
 
-#print ofLex_rat_cast /-
+#print ofLex_ratCast /-
 @[simp]
-theorem ofLex_rat_cast [HasRatCast α] (n : ℚ) : (ofLex n : α) = n :=
+theorem ofLex_ratCast [HasRatCast α] (n : ℚ) : (ofLex n : α) = n :=
   rfl
-#align of_lex_rat_cast ofLex_rat_cast
+#align of_lex_rat_cast ofLex_ratCast
 -/
 
diff --git a/Mathbin/Algebra/GeomSum.lean b/Mathbin/Algebra/GeomSum.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Neil Strickland. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Neil Strickland
 -/
-import Algebra.BigOperators.Order
+import Algebra.Order.BigOperators.Group.Finset
 import Algebra.BigOperators.Ring
 import Algebra.BigOperators.Intervals
 import Tactic.Abel

diff --git a/Mathbin/Algebra/GroupWithZero/NonZeroDivisors.lean b/Mathbin/Algebra/GroupWithZero/NonZeroDivisors.lean
@@ -217,7 +217,6 @@ theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective [NoZeroDivisors M'
 #align non_zero_divisors_le_comap_non_zero_divisors_of_injective nonZeroDivisors_le_comap_nonZeroDivisors_of_injective
 -/
 
-#print prod_zero_iff_exists_zero /-
 theorem prod_zero_iff_exists_zero [NoZeroDivisors M₁] [Nontrivial M₁] {s : Multiset M₁} :
     s.Prod = 0 ↔ ∃ (r : M₁) (hr : r ∈ s), r = 0 :=
   by
@@ -236,7 +235,6 @@ theorem prod_zero_iff_exists_zero [NoZeroDivisors M₁] [Nontrivial M₁] {s : M
       rintro b ⟨hb₁, hb₂⟩
       exact ⟨Multiset.mem_cons_of_mem hb₁, hb₂⟩
 #align prod_zero_iff_exists_zero prod_zero_iff_exists_zero
--/
 
 end nonZeroDivisors
 
diff --git a/Mathbin/Algebra/LinearRecurrence.lean b/Mathbin/Algebra/LinearRecurrence.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import Data.Polynomial.Eval
+import Algebra.Polynomial.Eval
 import LinearAlgebra.Dimension.Basic
 
 #align_import algebra.linear_recurrence from "leanprover-community/mathlib"@"814d76e2247d5ba8bc024843552da1278bfe9e5c"

diff --git a/Mathbin/Algebra/Module/Submodule/Ker.lean b/Mathbin/Algebra/Module/Submodule/Ker.lean
@@ -202,14 +202,10 @@ variable [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁
 
 variable (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃)
 
-/- warning: linear_map.map_sum clashes with add_monoid_hom.map_sum -> map_sumₓ
-Case conversion may be inaccurate. Consider using '#align linear_map.map_sum map_sumₓₓ'. -/
-#print map_sumₓ /-
 @[simp]
 theorem map_sum {ι : Type _} {t : Finset ι} {g : ι → M} : f (∑ i in t, g i) = ∑ i in t, f (g i) :=
   f.toAddMonoidHom.map_sum _ _
 #align linear_map.map_sum map_sumₓ
--/
 
 #print LinearMap.comp_assoc /-
 theorem comp_assoc (h : M₃ →ₛₗ[σ₃₄] M₄) :
@@ -2307,7 +2303,7 @@ variable {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPai
 
 variable (e e' : M ≃ₛₗ[σ₁₂] M₂)
 
-/- warning: linear_equiv.map_sum clashes with add_monoid_hom.map_sum -> map_sumₓ
+/- warning: linear_equiv.map_sum clashes with linear_map.map_sum -> map_sumₓ
 Case conversion may be inaccurate. Consider using '#align linear_equiv.map_sum map_sumₓₓ'. -/
 #print map_sumₓ /-
 @[simp]

diff --git a/Mathbin/Data/MvPolynomial/Basic.lean → Mathbin/Algebra/MvPolynomial/Basic.lean b/Mathbin/Data/MvPolynomial/Basic.lean → Mathbin/Algebra/MvPolynomial/Basic.lean
diff --git a/Mathbin/Data/MvPolynomial/Cardinal.lean → Mathbin/Algebra/MvPolynomial/Cardinal.lean b/Mathbin/Data/MvPolynomial/Cardinal.lean → Mathbin/Algebra/MvPolynomial/Cardinal.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Junyan Xu
 -/
 import Data.Finsupp.Fintype
-import Data.MvPolynomial.Equiv
+import Algebra.MvPolynomial.Equiv
 import SetTheory.Cardinal.Ordinal
 
 #align_import data.mv_polynomial.cardinal from "leanprover-community/mathlib"@"31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0"

diff --git a/Mathbin/Data/MvPolynomial/Comap.lean → Mathbin/Algebra/MvPolynomial/Comap.lean b/Mathbin/Data/MvPolynomial/Comap.lean → Mathbin/Algebra/MvPolynomial/Comap.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Data.MvPolynomial.Rename
+import Algebra.MvPolynomial.Rename
 
 #align_import data.mv_polynomial.comap from "leanprover-community/mathlib"@"932872382355f00112641d305ba0619305dc8642"
 

diff --git a/Mathbin/Data/MvPolynomial/CommRing.lean → Mathbin/Algebra/MvPolynomial/CommRing.lean b/Mathbin/Data/MvPolynomial/CommRing.lean → Mathbin/Algebra/MvPolynomial/CommRing.lean
@@ -3,7 +3,7 @@ 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, Johan Commelin, Mario Carneiro
 -/
-import Data.MvPolynomial.Degrees
+import Algebra.MvPolynomial.Degrees
 
 #align_import data.mv_polynomial.comm_ring from "leanprover-community/mathlib"@"2f5b500a507264de86d666a5f87ddb976e2d8de4"
 

diff --git a/Mathbin/Data/MvPolynomial/Counit.lean → Mathbin/Algebra/MvPolynomial/Counit.lean b/Mathbin/Data/MvPolynomial/Counit.lean → Mathbin/Algebra/MvPolynomial/Counit.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Data.MvPolynomial.Basic
+import Algebra.MvPolynomial.Basic
 
 #align_import data.mv_polynomial.counit from "leanprover-community/mathlib"@"932872382355f00112641d305ba0619305dc8642"
 

diff --git a/Mathbin/Data/MvPolynomial/Degrees.lean → Mathbin/Algebra/MvPolynomial/Degrees.lean b/Mathbin/Data/MvPolynomial/Degrees.lean → Mathbin/Algebra/MvPolynomial/Degrees.lean
@@ -3,8 +3,8 @@ 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, Johan Commelin, Mario Carneiro
 -/
-import Algebra.BigOperators.Order
-import Data.MvPolynomial.Rename
+import Algebra.Order.BigOperators.Group.Finset
+import Algebra.MvPolynomial.Rename
 
 #align_import data.mv_polynomial.variables from "leanprover-community/mathlib"@"2f5b500a507264de86d666a5f87ddb976e2d8de4"
 

diff --git a/Mathbin/Data/MvPolynomial/Derivation.lean → Mathbin/Algebra/MvPolynomial/Derivation.lean b/Mathbin/Data/MvPolynomial/Derivation.lean → Mathbin/Algebra/MvPolynomial/Derivation.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import Data.MvPolynomial.Supported
+import Algebra.MvPolynomial.Supported
 import RingTheory.Derivation.Basic
 
 #align_import data.mv_polynomial.derivation from "leanprover-community/mathlib"@"af471b9e3ce868f296626d33189b4ce730fa4c00"

diff --git a/Mathbin/Data/MvPolynomial/Division.lean → Mathbin/Algebra/MvPolynomial/Division.lean b/Mathbin/Data/MvPolynomial/Division.lean → Mathbin/Algebra/MvPolynomial/Division.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Algebra.MonoidAlgebra.Division
-import Data.MvPolynomial.Basic
+import Algebra.MvPolynomial.Basic
 
 #align_import data.mv_polynomial.division from "leanprover-community/mathlib"@"31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0"
 

diff --git a/Mathbin/Data/MvPolynomial/Equiv.lean → Mathbin/Algebra/MvPolynomial/Equiv.lean b/Mathbin/Data/MvPolynomial/Equiv.lean → Mathbin/Algebra/MvPolynomial/Equiv.lean
@@ -3,9 +3,9 @@ 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, Johan Commelin, Mario Carneiro
 -/
-import Data.MvPolynomial.Rename
-import Data.Polynomial.AlgebraMap
-import Data.MvPolynomial.Degrees
+import Algebra.MvPolynomial.Rename
+import Algebra.Polynomial.AlgebraMap
+import Algebra.MvPolynomial.Degrees
 import Data.Finsupp.Fin
 import Logic.Equiv.Fin
 import Algebra.BigOperators.Fin

diff --git a/Mathbin/Data/MvPolynomial/Expand.lean → Mathbin/Algebra/MvPolynomial/Expand.lean b/Mathbin/Data/MvPolynomial/Expand.lean → Mathbin/Algebra/MvPolynomial/Expand.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Robert Y. Lewis
 -/
-import Data.MvPolynomial.Monad
+import Algebra.MvPolynomial.Monad
 
 #align_import data.mv_polynomial.expand from "leanprover-community/mathlib"@"d64d67d000b974f0d86a2be7918cf800be6271c8"
 

diff --git a/Mathbin/Data/MvPolynomial/Funext.lean → Mathbin/Algebra/MvPolynomial/Funext.lean b/Mathbin/Data/MvPolynomial/Funext.lean → Mathbin/Algebra/MvPolynomial/Funext.lean
@@ -3,10 +3,10 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import Data.Polynomial.RingDivision
-import Data.MvPolynomial.Rename
+import Algebra.Polynomial.RingDivision
+import Algebra.MvPolynomial.Rename
 import RingTheory.Polynomial.Basic
-import Data.MvPolynomial.Polynomial
+import Algebra.MvPolynomial.Polynomial
 
 #align_import data.mv_polynomial.funext from "leanprover-community/mathlib"@"0b89934139d3be96f9dab477f10c20f9f93da580"
 

diff --git a/Mathbin/Data/MvPolynomial/Invertible.lean → Mathbin/Algebra/MvPolynomial/Invertible.lean b/Mathbin/Data/MvPolynomial/Invertible.lean → Mathbin/Algebra/MvPolynomial/Invertible.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Johan Commelin, Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Robert Y. Lewis
 -/
-import Data.MvPolynomial.Basic
+import Algebra.MvPolynomial.Basic
 import RingTheory.AlgebraTower
 
 #align_import data.mv_polynomial.invertible from "leanprover-community/mathlib"@"1dac236edca9b4b6f5f00b1ad831e35f89472837"

diff --git a/Mathbin/Data/MvPolynomial/Monad.lean → Mathbin/Algebra/MvPolynomial/Monad.lean b/Mathbin/Data/MvPolynomial/Monad.lean → Mathbin/Algebra/MvPolynomial/Monad.lean
@@ -3,8 +3,8 @@ Copyright (c) 2020 Johan Commelin, Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Robert Y. Lewis
 -/
-import Data.MvPolynomial.Rename
-import Data.MvPolynomial.Degrees
+import Algebra.MvPolynomial.Rename
+import Algebra.MvPolynomial.Degrees
 
 #align_import data.mv_polynomial.monad from "leanprover-community/mathlib"@"2f5b500a507264de86d666a5f87ddb976e2d8de4"
 

diff --git a/Mathbin/Data/MvPolynomial/PDeriv.lean → Mathbin/Algebra/MvPolynomial/PDeriv.lean b/Mathbin/Data/MvPolynomial/PDeriv.lean → Mathbin/Algebra/MvPolynomial/PDeriv.lean
@@ -3,8 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Yury Kudryashov
 -/
-import Data.MvPolynomial.Degrees
-import Data.MvPolynomial.Derivation
+import Algebra.MvPolynomial.Degrees
+import Algebra.MvPolynomial.Derivation
 
 #align_import data.mv_polynomial.pderiv from "leanprover-community/mathlib"@"5c1efce12ba86d4901463f61019832f6a4b1a0d0"
 

diff --git a/Mathbin/Data/MvPolynomial/Polynomial.lean → Mathbin/Algebra/MvPolynomial/Polynomial.lean b/Mathbin/Data/MvPolynomial/Polynomial.lean → Mathbin/Algebra/MvPolynomial/Polynomial.lean
@@ -3,8 +3,8 @@ Copyright (c) 2023 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Data.MvPolynomial.Equiv
-import Data.Polynomial.Eval
+import Algebra.MvPolynomial.Equiv
+import Algebra.Polynomial.Eval
 
 #align_import data.mv_polynomial.polynomial from "leanprover-community/mathlib"@"ef55335933293309ff8c0b1d20ffffeecbe5c39f"