fix

leanprover-community · Nov 24, 2024 · 124b15f · 124b15f
1 parent ce1696e
commit 124b15f
Show file tree

Hide file tree

Showing 6 changed files with 0 additions and 6 deletions.
diff --git a/Mathlib/Algebra/MvPolynomial/Equiv.lean b/Mathlib/Algebra/MvPolynomial/Equiv.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, Johan Commelin, Mario Carneiro
 -/
-import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.MvPolynomial.Rename
 import Mathlib.Algebra.MvPolynomial.Degrees
 import Mathlib.Algebra.Polynomial.AlgebraMap

diff --git a/Mathlib/Algebra/Polynomial/EraseLead.lean b/Mathlib/Algebra/Polynomial/EraseLead.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Alex Meiburg
 -/
-import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.Polynomial.Degree.Lemmas
 import Mathlib.Algebra.Polynomial.Degree.Monomial
 

diff --git a/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean b/Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
@@ -5,7 +5,6 @@ Authors: Joël Riou, Adam Topaz, Johan Commelin
 -/
 import Mathlib.Algebra.Homology.Additive
 import Mathlib.AlgebraicTopology.MooreComplex
-import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.CategoryTheory.Preadditive.Opposite
 import Mathlib.CategoryTheory.Idempotents.FunctorCategories
 

diff --git a/Mathlib/Combinatorics/Optimization/ValuedCSP.lean b/Mathlib/Combinatorics/Optimization/ValuedCSP.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 Martin Dvorak. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Martin Dvorak
 -/
-import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.Order.BigOperators.Group.Multiset
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.Matrix.Notation

diff --git a/Mathlib/Data/Nat/Choose/Multinomial.lean b/Mathlib/Data/Nat/Choose/Multinomial.lean
@@ -3,7 +3,6 @@ Copyright (c) 2022 Pim Otte. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller, Pim Otte
 -/
-import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.Order.Antidiag.Pi
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Data.Nat.Factorial.BigOperators

diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -3,7 +3,6 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp, Anne Baanen
 -/
-import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Data.Set.Subsingleton
 import Mathlib.Lean.Expr.ExtraRecognizers
 import Mathlib.LinearAlgebra.Prod