chore(LinearAlgebra/Span): split off definition of Submodule.span (#18618)

Vierkantor · Vierkantor · commit 9127890bca64 · 2024-11-15T15:51:55.000Z
This PR creates a new file `LinearAlgebra.Span.Defs` which contains the definition of a submodule span and some elementary results. Everything that needs heavier imports gets moved to `LinearAlgebra.Span.Basic`.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3369,7 +3369,8 @@ import Mathlib.LinearAlgebra.RootSystem.RootPositive
 import Mathlib.LinearAlgebra.SModEq
 import Mathlib.LinearAlgebra.Semisimple
 import Mathlib.LinearAlgebra.SesquilinearForm
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
+import Mathlib.LinearAlgebra.Span.Defs
 import Mathlib.LinearAlgebra.StdBasis
 import Mathlib.LinearAlgebra.SymplecticGroup
 import Mathlib.LinearAlgebra.TensorAlgebra.Basic
diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@@ -5,7 +5,7 @@ Authors: Jireh Loreaux
 -/
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Data.Set.UnionLift
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
 import Mathlib.RingTheory.NonUnitalSubring.Basic
 
 /-!
diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Anne Baanen
 -/
 import Mathlib.Algebra.Algebra.Equiv
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
 
 /-!
 # Towers of algebras
diff --git a/Mathlib/Algebra/Category/ModuleCat/Tannaka.lean b/Mathlib/Algebra/Category/ModuleCat/Tannaka.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Category.ModuleCat.Basic
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
 
 /-!
 # Tannaka duality for rings
diff --git a/Mathlib/Algebra/Module/Submodule/Bilinear.lean b/Mathlib/Algebra/Module/Submodule/Bilinear.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Eric Wieser
 -/
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
 import Mathlib.LinearAlgebra.BilinearMap
 
 /-!
diff --git a/Mathlib/LinearAlgebra/Basis/Defs.lean b/Mathlib/LinearAlgebra/Basis/Defs.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Alexander Bentkamp
 -/
 import Mathlib.LinearAlgebra.Finsupp.LinearCombination
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
 
 /-!
 # Bases
diff --git a/Mathlib/LinearAlgebra/FiniteSpan.lean b/Mathlib/LinearAlgebra/FiniteSpan.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash, Deepro Choudhury
 -/
 import Mathlib.GroupTheory.OrderOfElement
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Defs
 import Mathlib.Algebra.Module.Equiv.Basic
 
 /-!
diff --git a/Mathlib/LinearAlgebra/Finsupp/Span.lean b/Mathlib/LinearAlgebra/Finsupp/Span.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.LinearAlgebra.Finsupp.Defs
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
 
 /-!
 # Finitely supported functions and spans
diff --git a/Mathlib/LinearAlgebra/Finsupp/Supported.lean b/Mathlib/LinearAlgebra/Finsupp/Supported.lean
@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.Module.Submodule.Range
 import Mathlib.LinearAlgebra.Finsupp.LSum
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Defs
 
 /-!
 # `Finsupp`s supported on a given submodule
diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Eric Wieser
 -/
 import Mathlib.Algebra.Algebra.Prod
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
 import Mathlib.Order.PartialSups
 
 /-! ### Products of modules
diff --git a/Mathlib/LinearAlgebra/Quotient/Basic.lean b/Mathlib/LinearAlgebra/Quotient/Basic.lean
@@ -7,7 +7,7 @@ import Mathlib.Algebra.Module.Equiv.Basic
 import Mathlib.GroupTheory.QuotientGroup.Basic
 import Mathlib.LinearAlgebra.Pi
 import Mathlib.LinearAlgebra.Quotient.Defs
-import Mathlib.LinearAlgebra.Span
+import Mathlib.LinearAlgebra.Span.Basic
 import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
diff --git a/Mathlib/LinearAlgebra/Span/Basic.lean b/Mathlib/LinearAlgebra/Span/Basic.lean
diff --git a/Mathlib/LinearAlgebra/Span/Defs.lean b/Mathlib/LinearAlgebra/Span/Defs.lean
diff --git a/Mathlib/RingTheory/Ideal/AssociatedPrime.lean b/Mathlib/RingTheory/Ideal/AssociatedPrime.lean
diff --git a/Mathlib/RingTheory/Ideal/Span.lean b/Mathlib/RingTheory/Ideal/Span.lean
