chore(LinearAlgebra/Span): reverse import order between Submodule/Pointwise and Span/Basic

[martinwintermath]

• Revert import order between Span/Basic and Submodule/Pointwise
• Remove import Submodule/Pointwise throughout mathlib because already imported via Span/Basic
• Move lemmas from Submodule/Pointwise to Span/Basic when they require the Span/Basic-import (except for span_neg_eq_neg which was moved for a different reason, see below).
• Rewriting part of Span/Basic to use pointwise notation (this was previously done for sets, and now it can be done for submodules as well). Adjust proofs to this change.
• use moved span_neg_eq_neg to shorten proof of span_neg.

This is a follow up on #36689 in which the wrong import order was noted.

---

[github-actions]

PR summary 8ec19128ad

Import changes exceeding 2%

%	File
+21.51%	Mathlib.LinearAlgebra.Span.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Span.Basic	767	932	+165 (+21.51%)
Mathlib.Algebra.Module.Submodule.Pointwise	932	897	-35 (-3.76%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Module.Submodule.Pointwise	-35
29 files Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.KInjective Mathlib.Algebra.Homology.DerivedCategory.KProjective Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.EulerCharacteristic Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Ext Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity Mathlib.Data.Matrix.Cartan Mathlib.LinearAlgebra.Alternating.Uncurry.Fin Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.Topology.ContinuousMap.Periodic	1
Mathlib.GroupTheory.CosetCover	2
158 files Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.AlgebraicTopology.SimplicialSet.TopAdj Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Analysis.Asymptotics.Completion Mathlib.Analysis.Asymptotics.Lemmas Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Analysis.Calculus.FDeriv.Defs Mathlib.Analysis.Calculus.TangentCone.DimOne Mathlib.Analysis.Calculus.TangentCone.Pi Mathlib.Analysis.Calculus.TangentCone.ProperSpace Mathlib.Analysis.Calculus.TangentCone.Real Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Convex.ContinuousLinearEquiv Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.Independent Mathlib.Analysis.Convex.Jensen Mathlib.Analysis.Convex.MetricSpace Mathlib.Analysis.Convex.PathConnected Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.StdSimplex Mathlib.Analysis.Convex.StoneSeparation Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Convex.Topology Mathlib.Analysis.Convex.TotallyBounded Mathlib.Analysis.Fourier.Notation Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.Ceva Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Affine.Simplex Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Field.Instances Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.FunctionSeries Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.SeparationQuotient Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Module.Ball.Action Mathlib.Analysis.Normed.Module.Ball.RadialEquiv Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Extr Mathlib.Analysis.Normed.Module.RCLike.Real Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.Shrink Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Module.TransferInstance Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.Normed.Operator.Conformal Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Ring.InfiniteSum Mathlib.Analysis.Normed.Ring.Int Mathlib.Analysis.Normed.Ring.Lemmas Mathlib.Analysis.Normed.Ring.Ultra Mathlib.Analysis.Seminorm Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Tactic.ComputeAsymptotics.Lemmas Mathlib.Topology.Algebra.AffineSubspace Mathlib.Topology.Algebra.ContinuousAffineEquiv Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.CompactOpen Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.LinearMapCompletion Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.ClosedSubmodule Mathlib.Topology.Algebra.Module.Compact Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.PerfectPairing Mathlib.Topology.Algebra.Module.Spaces.WeakBilin Mathlib.Topology.Algebra.Module.Spaces.WeakDual Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.TransferInstance Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional Mathlib.Topology.Algebra.SeparationQuotient.Hom Mathlib.Topology.Algebra.TopologicallyNilpotent Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.CWComplex.Classical.Basic Mathlib.Topology.CWComplex.Classical.Finite Mathlib.Topology.CWComplex.Classical.Subcomplex Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.LocallyConvex Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.Homotopy.Affine Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Lifting Mathlib.Topology.Homotopy.LocallyContractible Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.Homotopy.TopCat.ToSSet Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.MetricSpace.Algebra Mathlib.Topology.MetricSpace.Completion Mathlib.Topology.Sion Mathlib.Topology.Subpath Mathlib.Topology.UniformSpace.Dini Mathlib.Topology.UniformSpace.ProdApproximation	4
92 files Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Stalk Mathlib.Algebra.Colimit.Finiteness Mathlib.Algebra.Colimit.TensorProduct Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.AlgebraicTopology.SimplicialComplex.Basic Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.LinearAlgebra.AffineSpace.Ceva Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.DirectSum.Finite Mathlib.LinearAlgebra.Quotient.Bilinear Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.CoassocSimps Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Coalgebra.MulOpposite Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.RingTheory.Finiteness.Finsupp Mathlib.RingTheory.Ideal.Quotient.Basic Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.Morita.Matrix Mathlib.Topology.Sheaves.Abelian Mathlib.Topology.Sheaves.AddCommGrpCat Mathlib.Topology.Sheaves.Flasque Mathlib.Topology.Sheaves.MayerVietoris	6
4 files Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length	9
Mathlib.GroupTheory.Coxeter.Basic Mathlib.LinearAlgebra.Alternating.DomCoprod	14
Mathlib.Analysis.Normed.Ring.Finite	15
Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.FunctionTopology	16
15 files Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.NNReal Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Star Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Geometry.Convex.Cone.Basic Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.Algebra.Monoid.FunOnFinite	17
8 files Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Analysis.Calculus.TangentCone.Prod Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.Dimension.Subsingleton Mathlib.Topology.Algebra.Group.Extension	18
57 files Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Colimit.Module Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.OfFn Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.SkewMonoidAlgebra.Lift Mathlib.Algebra.SkewMonoidAlgebra.Single Mathlib.Algebra.SkewMonoidAlgebra.Support Mathlib.Algebra.SkewPolynomial.Basic Mathlib.Analysis.Convex.Segment Mathlib.FieldTheory.IsRealClosed.Basic Mathlib.FieldTheory.RatFunc.Defs Mathlib.LinearAlgebra.AffineSpace.Centroid Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.Curry Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Basis.Submodule Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.ConvexSpace.AffineSpace Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.LinearIndependent.Lemmas Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.DirectSum Mathlib.LinearAlgebra.Multilinear.Finsupp Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp Mathlib.LinearAlgebra.PiTensorProduct.DirectSum Mathlib.LinearAlgebra.PiTensorProduct.Finsupp Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.SesquilinearForm.Basic Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorProduct.Decomposition Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.LinearAlgebra.TensorProduct.Free Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.Ideal.Basis Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Polynomial.Pochhammer	19
7 files Mathlib.Algebra.Polynomial.Cardinal Mathlib.Computability.TMComputable Mathlib.Computability.TuringMachine.Computable Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.SModEq.Basic Mathlib.LinearAlgebra.SModEq	20
69 files Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Exact Mathlib.Algebra.FiveLemma Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Module Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.CoeffList Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Defs Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Analysis.Normed.Lp.WithLp Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.Data.Nat.Choose.Vandermonde Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Basis.SMul Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.Isomorphisms Mathlib.LinearAlgebra.LeftExact Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Pi Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Ideal.Basic Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Subring Mathlib.Tactic.ComputeDegree	21
Mathlib.Analysis.Calculus.TangentCone.Basic	24
15 files Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Reflection Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.ConjTranspose Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.Hadamard Mathlib.LinearAlgebra.Matrix.Notation Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.RowCol Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.Trace	27
Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Topology.Algebra.Affine	30
6 files Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Field.TransferInstance Mathlib.Analysis.Normed.Ring.Basic Mathlib.Analysis.Normed.Ring.TransferInstance Mathlib.Topology.MetricSpace.CauSeqFilter	31
3 files Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered	33
24 files Mathlib.Algebra.Algebra.Subalgebra.Matrix Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Composition Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Matrix.Module Mathlib.LinearAlgebra.Matrix.Unique Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.TensorPower.Symmetric Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.RingTheory.PiTensorProduct Mathlib.Tactic.Module Mathlib.Topology.LocallyConstant.Algebra	34
Mathlib.NumberTheory.Multiplicity Mathlib.RingTheory.Localization.NumDen	53
3 files Mathlib.RingTheory.Finiteness.Bilinear Mathlib.RingTheory.Finiteness.Defs Mathlib.RingTheory.Finiteness.Prod	64
Mathlib.GroupTheory.DivisibleHull	66
Mathlib.Algebra.MonoidAlgebra.Ideal	67
Mathlib.RingTheory.Localization.Cardinality	71
Mathlib.RingTheory.Localization.FractionRing	77
3 files Mathlib.Algebra.RingQuot Mathlib.Algebra.Star.RingQuot Mathlib.RingTheory.Localization.Basic	79
4 files Mathlib.Algebra.Module.LocalizedModule.AtPrime Mathlib.Algebra.Module.LocalizedModule.Away Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.IsLocalization	80
Mathlib.NumberTheory.Basic	83
6 files Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.Ideal.Nonunits Mathlib.RingTheory.Ideal.Span Mathlib.RingTheory.LocalRing.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.Spectrum.Maximal.Defs	98
Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Star.TensorProduct	110
3 files Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric	114
Mathlib.Algebra.Star.Module	118
Mathlib.Algebra.Star.NonUnitalSubalgebra	120
Mathlib.Algebra.Algebra.Subalgebra.Order	122
Mathlib.Algebra.Category.ModuleCat.Algebra	132
5 files Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Tower	134
Mathlib.Algebra.Category.ModuleCat.Tannaka	137
3 files Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Defs Mathlib.LinearAlgebra.TensorProduct.Map	139
7 files Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Tower Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Prod Mathlib.Tactic.Algebraize	142
Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.LinearAlgebra.Span.Basic	165

---

Declarations diff

+ instance : IsModularLattice (Submodule R M) := ⟨
+ ofSubmodule_neg
- instance : IsModularLattice (Submodule R M) := ⟨fun x _ hxy _ _ => by

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[ocfnash]

Thanks for working on this.

The import change for Mathlib.LinearAlgebra.Span.Basic is quite big (767 jumps to 932). Given that this file sits somewhat in the middle of Mathlib I think we should try to brings this down a little.

One possibility which I see is that we could reduce the imports of Mathlib.Algebra.Module.Submodule.Pointwise as follows:

- public import Mathlib.LinearAlgebra.Finsupp.Supported
+ public import Mathlib.Algebra.Module.Submodule.Range

A handful of lemmas like Submodule.set_smul_eq_map will break but we could place these in a new file Mathlib.Algebra.Module.Submodule.Finsupp.

This sort of work is annoyingly-manual and not fun but I think it would be worth at least one attempt to see how this affects things.

What do you think?