chore: Move LinearMap.ker to a new file (#10233)

This shortens `Mathlib.LinearAlgebra.Basic`, which is both longer than we like and doesn't have a clear scope.
leanprover-community · Feb 18, 2024 · c85a97d · c85a97d
1 parent 63bf251
commit c85a97d
Show file tree

Hide file tree

Showing 19 changed files with 462 additions and 290 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -341,6 +341,7 @@ import Mathlib.Algebra.Module.Prod
 import Mathlib.Algebra.Module.Projective
 import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.Module.Submodule.Bilinear
+import Mathlib.Algebra.Module.Submodule.Ker
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Algebra.Module.Submodule.LinearMap
 import Mathlib.Algebra.Module.Submodule.Localization

diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean
@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import Mathlib.Algebra.CharZero.Lemmas
+import Mathlib.Algebra.Module.Submodule.Ker
+import Mathlib.Algebra.Module.Submodule.RestrictScalars
 import Mathlib.Algebra.Module.ULift
-import Mathlib.LinearAlgebra.Basic
 import Mathlib.RingTheory.Subring.Basic
-import Mathlib.Algebra.Module.Submodule.RestrictScalars
 
 #align_import algebra.algebra.basic from "leanprover-community/mathlib"@"36b8aa61ea7c05727161f96a0532897bd72aedab"
 

diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@@ -5,6 +5,7 @@ Authors: Jireh Loreaux
 -/
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Data.Set.UnionLift
+import Mathlib.LinearAlgebra.Basic
 import Mathlib.LinearAlgebra.Span
 import Mathlib.RingTheory.NonUnitalSubring.Basic
 

diff --git a/Mathlib/Algebra/Algebra/Operations.lean b/Mathlib/Algebra/Algebra/Operations.lean
@@ -6,15 +6,16 @@ Authors: Kenny Lau
 import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Algebra.Opposite
-import Mathlib.Algebra.Module.Submodule.Pointwise
-import Mathlib.Algebra.Module.Submodule.Bilinear
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.Module.Opposites
+import Mathlib.Algebra.Module.Submodule.Bilinear
+import Mathlib.Algebra.Module.Submodule.Pointwise
 import Mathlib.Algebra.Order.Kleene
 import Mathlib.Data.Finset.Pointwise
-import Mathlib.Data.Set.Semiring
 import Mathlib.Data.Set.Pointwise.BigOperators
+import Mathlib.Data.Set.Semiring
 import Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
-import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
+import Mathlib.LinearAlgebra.Basic
 
 #align_import algebra.algebra.operations from "leanprover-community/mathlib"@"27b54c47c3137250a521aa64e9f1db90be5f6a26"
 

diff --git a/Mathlib/Algebra/Algebra/Prod.lean b/Mathlib/Algebra/Algebra/Prod.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import Mathlib.Algebra.Algebra.Hom
+import Mathlib.Algebra.Module.Prod
 
 #align_import algebra.algebra.prod from "leanprover-community/mathlib"@"28aa996fc6fb4317f0083c4e6daf79878d81be33"
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.CategoryTheory.Conj
 import Mathlib.CategoryTheory.Linear.Basic
 import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
+import Mathlib.LinearAlgebra.Basic
 
 #align_import algebra.category.Module.basic from "leanprover-community/mathlib"@"829895f162a1f29d0133f4b3538f4cd1fb5bffd3"