[Merged by Bors] - feat: strengthen Cayley-Hamilton by artie2000 · Pull Request #37872 · leanprover-community/mathlib4

artie2000 · 2026-04-10T01:42:34Z

Strengthen the statement of Cayley-Hamilton to bound the degree of the annihilating polynomial by the number of generators
Generalise minpoly.natDegree_le to non-free modules: minpoly.natDegree_le_spanFinrank

github-actions · 2026-04-10T01:43:32Z

PR summary 2c53994ec0

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Valuation.Minpoly	1727	1632	-95 (-5.50%)
Mathlib.RingTheory.IsAdjoinRoot	1726	1675	-51 (-2.95%)
Mathlib.FieldTheory.Normal.Basic	1726	1689	-37 (-2.14%)
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap	1556	1559	+3 (+0.19%)
Mathlib.LinearAlgebra.Charpoly.Basic	1677	1680	+3 (+0.18%)

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.Valuation.Minpoly`	-95
`Mathlib.RingTheory.IsAdjoinRoot`	-51
`Mathlib.NumberTheory.KummerDedekind`	-47
`Mathlib.FieldTheory.Normal.Basic` `Mathlib.FieldTheory.Normal.Closure`	-37
572 files `Mathlib.Algebra.Category.ModuleCat.Descent` `Mathlib.Algebra.Category.Ring.EqualizerPushout` `Mathlib.Algebra.Category.Ring.Under.Limits` `Mathlib.Algebra.Lie.AdjointAction.Basic` `Mathlib.Algebra.Lie.Basis` `Mathlib.Algebra.Lie.CartanExists` `Mathlib.Algebra.Lie.Derivation.Killing` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.Algebra.Lie.Engel` `Mathlib.Algebra.Lie.Killing` `Mathlib.Algebra.Lie.LieTheorem` `Mathlib.Algebra.Lie.Rank` `Mathlib.Algebra.Lie.Semisimple.Lemmas` `Mathlib.Algebra.Lie.TraceForm` `Mathlib.Algebra.Lie.Weights.Basic` `Mathlib.Algebra.Lie.Weights.Cartan` `Mathlib.Algebra.Lie.Weights.Chain` `Mathlib.Algebra.Lie.Weights.IsSimple` `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Lie.Weights.Linear` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.Algebra.Order.Ring.StandardPart` `Mathlib.Algebra.Polynomial.Bivariate` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.AlgClosed.Basic` `Mathlib.AlgebraicGeometry.Artinian` `Mathlib.AlgebraicGeometry.ColimitsOver` `Mathlib.AlgebraicGeometry.Cover.Directed` `Mathlib.AlgebraicGeometry.Cover.MorphismProperty` `Mathlib.AlgebraicGeometry.Cover.Open` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.QuasiCompact` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.EffectiveEpi` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree` `Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula` `Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point` `Mathlib.AlgebraicGeometry.EllipticCurve.Reduction` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.GammaSpecAdjunction` `Mathlib.AlgebraicGeometry.Geometrically.Basic` `Mathlib.AlgebraicGeometry.Geometrically.Connected` `Mathlib.AlgebraicGeometry.Geometrically.Integral` `Mathlib.AlgebraicGeometry.Geometrically.Irreducible` `Mathlib.AlgebraicGeometry.Geometrically.Reduced` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Gluing` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Functorial` `Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.LimitsOver` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Modules.Presheaf` `Mathlib.AlgebraicGeometry.Modules.Sheaf` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Descent` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.FlatDescent` `Mathlib.AlgebraicGeometry.Morphisms.FlatMono` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.LocalClosure` `Mathlib.AlgebraicGeometry.Morphisms.LocalIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.OpenImmersion` `Mathlib.AlgebraicGeometry.Over` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.QuasiAffine` `Mathlib.AlgebraicGeometry.RationalMap` `Mathlib.AlgebraicGeometry.RelativeGluing` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Restrict` `Mathlib.AlgebraicGeometry.Scheme` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.ConstantSheaf` `Mathlib.AlgebraicGeometry.Sites.Fpqc` `Mathlib.AlgebraicGeometry.Sites.MorphismProperty` `Mathlib.AlgebraicGeometry.Sites.Pretopology` `Mathlib.AlgebraicGeometry.Sites.QuasiCompact` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.Spec` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.StructureSheaf` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart` `Mathlib.Analysis.CStarAlgebra.Fuglede` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.PositiveLinearMap` `Mathlib.Analysis.CStarAlgebra.Projection` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.CStarAlgebra.Unitary.Connected` `Mathlib.Analysis.CStarAlgebra.Unitary.Span` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.GaussLucas` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Measure` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.InnerProductSpace.GramMatrix` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Reproducing` `Mathlib.Analysis.InnerProductSpace.Semisimple` `Mathlib.Analysis.InnerProductSpace.SingularValues` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.StandardSubspace` `Mathlib.Analysis.InnerProductSpace.Trace` `Mathlib.Analysis.Matrix.HermitianFunctionalCalculus` `Mathlib.Analysis.Matrix.LDL` `Mathlib.Analysis.Matrix.Order` `Mathlib.Analysis.Matrix.PosDef` `Mathlib.Analysis.Matrix.Spectrum` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.GelfandFormula` `Mathlib.Analysis.Normed.Algebra.GelfandMazur` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Normed.Field.Dense` `Mathlib.Analysis.Normed.Field.Krasner` `Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv` `Mathlib.Analysis.Normed.Unbundled.SpectralNorm` `Mathlib.Analysis.Polynomial.Factorization` `Mathlib.Analysis.Polynomial.MahlerMeasure` `Mathlib.Analysis.Real.Hyperreal` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder` `Mathlib.CategoryTheory.Preadditive.Schur` `Mathlib.Combinatorics.Additive.ErdosGinzburgZiv` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.AlgebraicClosure` `Mathlib.FieldTheory.AxGrothendieck` `Mathlib.FieldTheory.CardinalEmb` `Mathlib.FieldTheory.Cardinality` `Mathlib.FieldTheory.ChevalleyWarning` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.FieldTheory.Differential.Liouville` `Mathlib.FieldTheory.Extension` `Mathlib.FieldTheory.Finite.Basic` `Mathlib.FieldTheory.Finite.Extension` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.FieldTheory.Finite.Polynomial` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Finite.Valuation` `Mathlib.FieldTheory.Galois.Abelian` `Mathlib.FieldTheory.Galois.Basic` `Mathlib.FieldTheory.Galois.GaloisClosure` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.IsGaloisGroup` `Mathlib.FieldTheory.Galois.NormalBasis` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.IntermediateField.Adjoin.Basic` `Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure` `Mathlib.FieldTheory.IsAlgClosed.Basic` `Mathlib.FieldTheory.IsAlgClosed.Classification` `Mathlib.FieldTheory.IsAlgClosed.Spectrum` `Mathlib.FieldTheory.IsPerfectClosure` `Mathlib.FieldTheory.IsSepClosed` `Mathlib.FieldTheory.Isaacs` `Mathlib.FieldTheory.JacobsonNoether` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.KummerExtension` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.LinearDisjoint` `Mathlib.FieldTheory.Minpoly.ConjRootClass` `Mathlib.FieldTheory.Minpoly.IsConjRoot` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.NormalizedTrace` `Mathlib.FieldTheory.PerfectClosure` `Mathlib.FieldTheory.Perfect` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.FieldTheory.PrimitiveElement` `Mathlib.FieldTheory.PurelyInseparable.Basic` `Mathlib.FieldTheory.PurelyInseparable.Exponent` `Mathlib.FieldTheory.PurelyInseparable.PerfectClosure` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.RatFunc.IntermediateField` `Mathlib.FieldTheory.RatFunc.Luroth` `Mathlib.FieldTheory.RatFunc.Valuation` `Mathlib.FieldTheory.Relrank` `Mathlib.FieldTheory.SeparableClosure` `Mathlib.FieldTheory.SeparableDegree` `Mathlib.FieldTheory.SeparablyGenerated` `Mathlib.GroupTheory.SpecificGroups.ZGroup` `Mathlib.LinearAlgebra.Eigenspace.Charpoly` `Mathlib.LinearAlgebra.Eigenspace.Pi` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.LinearAlgebra.Eigenspace.Triangularizable` `Mathlib.LinearAlgebra.JordanChevalley` `Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs` `Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField` `Mathlib.LinearAlgebra.QuadraticForm.AlgClosed` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.BaseExists` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Chain` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.G2` `Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.Irreducible` `Mathlib.LinearAlgebra.RootSystem.IsValuedIn` `Mathlib.LinearAlgebra.RootSystem.Reduced` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.LinearAlgebra.Semisimple` `Mathlib.ModelTheory.Algebra.Field.IsAlgClosed` `Mathlib.ModelTheory.Algebra.Ring.Definability` `Mathlib.NumberTheory.ArithmeticFunction.Carmichael` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.FermatPsp` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Height.NumberField` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LSeries.ZetaZeros` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.Basic` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LocalField.Basic` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.MahlerMeasure` `Mathlib.NumberTheory.ModularForms.BoundedAtCusp` `Mathlib.NumberTheory.ModularForms.Cusps` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion.FinitePlace` `Mathlib.NumberTheory.NumberField.Completion.InfinitePlace` `Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances` `Mathlib.NumberTheory.NumberField.Completion.Ramification` `Mathlib.NumberTheory.NumberField.Cyclotomic.Basic` `Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings` `Mathlib.NumberTheory.NumberField.Cyclotomic.Galois` `Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal` `Mathlib.NumberTheory.NumberField.Cyclotomic.PID` `Mathlib.NumberTheory.NumberField.Cyclotomic.Three` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind` `Mathlib.NumberTheory.NumberField.InfiniteAdeleRing` `Mathlib.NumberTheory.NumberField.InfinitePlace.Basic` `Mathlib.NumberTheory.NumberField.InfinitePlace.Completion` `Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings` `Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification` `Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Padics.Complex` `Mathlib.NumberTheory.Padics.HeightOneSpectrum` `Mathlib.NumberTheory.Padics.WithVal` `Mathlib.NumberTheory.PowModTotient` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Basic` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.RamificationInertia.HilbertTheory` `Mathlib.NumberTheory.RamificationInertia.Inertia` `Mathlib.NumberTheory.RamificationInertia.Ramification` `Mathlib.NumberTheory.RamificationInertia.Unramified` `Mathlib.NumberTheory.RatFunc.Ostrowski` `Mathlib.NumberTheory.SumFourSquares` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.Wilson` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.Probability.Distributions.Gaussian.CharFun` `Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence` `Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence` `Mathlib.Probability.Distributions.Gaussian.Multivariate` `Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess` `Mathlib.Probability.Moments.CovarianceBilin` `Mathlib.RepresentationTheory.AlgebraRepresentation.Basic` `Mathlib.RepresentationTheory.Character` `Mathlib.RepresentationTheory.FDRep` `Mathlib.RepresentationTheory.FinGroupCharZero` `Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree` `Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic` `Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality` `Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence` `Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree` `Mathlib.RepresentationTheory.Invariants` `Mathlib.RepresentationTheory.Irreducible` `Mathlib.RepresentationTheory.Tannaka` `Mathlib.RingTheory.AdicCompletion.Noetherian` `Mathlib.RingTheory.Adjoin.Polynomial.Bivariate` `Mathlib.RingTheory.Algebraic.StronglyTranscendental` `Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure` `Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.GaussLemma` `Mathlib.RingTheory.DedekindDomain.Instances` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.LinearDisjoint` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.Locus` `Mathlib.RingTheory.Etale.QuasiFinite` `Mathlib.RingTheory.Etale.StandardEtale` `Mathlib.RingTheory.Finiteness.Descent` `Mathlib.RingTheory.Flat.FaithfullyFlat.Descent` `Mathlib.RingTheory.Flat.Rank` `Mathlib.RingTheory.Flat.TorsionFree` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Frobenius` `Mathlib.RingTheory.Grassmannian` `Mathlib.RingTheory.HopkinsLevitzki` `Mathlib.RingTheory.Ideal.GoingDown` `Mathlib.RingTheory.Ideal.Int` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients` `Mathlib.RingTheory.IntegralClosure.GoingDown` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.Invariant.Basic` `Mathlib.RingTheory.Invariant.Profinite` `Mathlib.RingTheory.Jacobson.Artinian` `Mathlib.RingTheory.KrullDimension.LocalRing` `Mathlib.RingTheory.KrullDimension.Module` `Mathlib.RingTheory.KrullDimension.Zero` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalRing.ResidueField.Fiber` `Mathlib.RingTheory.LocalRing.ResidueField.Polynomial` `Mathlib.RingTheory.Localization.AtPrime.Extension` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Localization.Pi` `Mathlib.RingTheory.Nilpotent.GeometricallyReduced` `Mathlib.RingTheory.Norm.Basic` `Mathlib.RingTheory.Norm.Transitivity` `Mathlib.RingTheory.NormalClosure` `Mathlib.RingTheory.Nullstellensatz` `Mathlib.RingTheory.OrderOfVanishing.Basic` `Mathlib.RingTheory.OrderOfVanishing.Noetherian` `Mathlib.RingTheory.Perfection` `Mathlib.RingTheory.Perfectoid.BDeRham` `Mathlib.RingTheory.Perfectoid.FontaineTheta` `Mathlib.RingTheory.Perfectoid.Untilt` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.QuasiFinite.Basic` `Mathlib.RingTheory.QuasiFinite.Polynomial` `Mathlib.RingTheory.QuasiFinite.Weakly` `Mathlib.RingTheory.RingHom.Etale` `Mathlib.RingTheory.RingHom.FaithfullyFlat` `Mathlib.RingTheory.RingHom.Flat` `Mathlib.RingTheory.RingHom.LocallyStandardSmooth` `Mathlib.RingTheory.RingHom.QuasiFinite` `Mathlib.RingTheory.RingHom.Smooth` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.RingTheory.SimpleModule.IsAlgClosed` `Mathlib.RingTheory.Smooth.Fiber` `Mathlib.RingTheory.Smooth.Field` `Mathlib.RingTheory.Smooth.Flat` `Mathlib.RingTheory.Smooth.IntegralClosure` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.NoetherianDescent` `Mathlib.RingTheory.Smooth.Quotient` `Mathlib.RingTheory.Smooth.StandardSmoothOfFree` `Mathlib.RingTheory.Spectrum.Maximal.Topology` `Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity` `Mathlib.RingTheory.Spectrum.Prime.Chevalley` `Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Spectrum.Prime.Homeomorph` `Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC` `Mathlib.RingTheory.Spectrum.Prime.Jacobson` `Mathlib.RingTheory.Spectrum.Prime.Module` `Mathlib.RingTheory.Spectrum.Prime.Noetherian` `Mathlib.RingTheory.Spectrum.Prime.Polynomial` `Mathlib.RingTheory.Spectrum.Prime.TensorProduct` `Mathlib.RingTheory.Spectrum.Prime.Topology` `Mathlib.RingTheory.Teichmuller` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Dedekind` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.LocalStructure` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Valuation.AlgebraInstances` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.Discrete.RankOne` `Mathlib.RingTheory.Valuation.Extension` `Mathlib.RingTheory.Valuation.FiniteField` `Mathlib.RingTheory.Valuation.LocalSubring` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.RingTheory.WittVector.Basic` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.RingTheory.WittVector.Complete` `Mathlib.RingTheory.WittVector.Defs` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.RingTheory.WittVector.Domain` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.RingTheory.WittVector.Frobenius` `Mathlib.RingTheory.WittVector.Identities` `Mathlib.RingTheory.WittVector.InitTail` `Mathlib.RingTheory.WittVector.IsPoly` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.RingTheory.WittVector.MulCoeff` `Mathlib.RingTheory.WittVector.MulP` `Mathlib.RingTheory.WittVector.StructurePolynomial` `Mathlib.RingTheory.WittVector.TeichmullerSeries` `Mathlib.RingTheory.WittVector.Teichmuller` `Mathlib.RingTheory.WittVector.Truncated` `Mathlib.RingTheory.WittVector.Verschiebung` `Mathlib.RingTheory.ZMod.Torsion` `Mathlib.RingTheory.ZMod.UnitsCyclic` `Mathlib.RingTheory.ZariskisMainTheorem` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic` `Mathlib.Topology.Algebra.Ring.Compact` `Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuativeRel` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Algebra.Valued.WithVal` `Mathlib.Topology.Algebra.Valued.WithZeroMulInt` `Mathlib.Topology.Compactification.OnePoint.ProjectiveLine`	1
78 files `Mathlib.AlgebraicGeometry.Group.Abelian` `Mathlib.AlgebraicGeometry.Group.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite` `Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale` `Mathlib.AlgebraicGeometry.Normalization` `Mathlib.AlgebraicGeometry.Sites.ElladicCohomology` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.Proetale` `Mathlib.AlgebraicGeometry.ZariskisMainTheorem` `Mathlib.Analysis.AbsoluteValue.Equivalence` `Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.Normed.Field.WithAbs` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema` `Mathlib.FieldTheory.Fixed` `Mathlib.FieldTheory.KummerPolynomial` `Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed` `Mathlib.FieldTheory.Separable` `Mathlib.FieldTheory.SplittingField.Construction` `Mathlib.FieldTheory.SplittingField.IsSplittingField` `Mathlib.LinearAlgebra.FreeModule.Norm` `Mathlib.LinearAlgebra.Matrix.Charpoly.Disc` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo` `Mathlib.LinearAlgebra.Projectivization.Action` `Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.Bounds` `Mathlib.NumberTheory.ModularForms.CongruenceSubgroups` `Mathlib.NumberTheory.ModularForms.DedekindEta` `Mathlib.NumberTheory.ModularForms.Delta` `Mathlib.NumberTheory.ModularForms.Derivative` `Mathlib.NumberTheory.ModularForms.Discriminant` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.NormTrace` `Mathlib.NumberTheory.ModularForms.Petersson` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Ostrowski` `Mathlib.RingTheory.Adjoin.Field` `Mathlib.RingTheory.AdjoinRoot` `Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis` `Mathlib.RingTheory.Derivation.MapCoeffs` `Mathlib.RingTheory.Etale.Basic` `Mathlib.RingTheory.Etale.Kaehler` `Mathlib.RingTheory.Etale.Pi` `Mathlib.RingTheory.Extension.Cotangent.Basis` `Mathlib.RingTheory.Extension.Cotangent.LocalizationAway` `Mathlib.RingTheory.Finiteness.FinitePresentationLocal` `Mathlib.RingTheory.Finiteness.ModuleFinitePresentation` `Mathlib.RingTheory.LocalRing.ResidueField.Instances` `Mathlib.RingTheory.Localization.Away.AdjoinRoot` `Mathlib.RingTheory.PicardGroup` `Mathlib.RingTheory.Polynomial.GaussLemma` `Mathlib.RingTheory.Polynomial.IsIntegral` `Mathlib.RingTheory.Polynomial.Resultant.Basic` `Mathlib.RingTheory.Polynomial.SeparableDegree` `Mathlib.RingTheory.Polynomial.UniversalFactorizationRing` `Mathlib.RingTheory.RingHom.FinitePresentation` `Mathlib.RingTheory.Smooth.AdicCompletion` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.RingTheory.Smooth.StandardSmoothCotangent` `Mathlib.RingTheory.TotallySplit` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.Topology.Algebra.Group.Matrix`	2
53 files `Mathlib.Algebra.GCDMonoid.IntegrallyClosed` `Mathlib.Algebra.Module.DedekindDomain` `Mathlib.Algebra.Module.LinearMap.Polynomial` `Mathlib.Algebra.Module.PID` `Mathlib.Algebra.Module.Torsion.PrimaryComponent` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra` `Mathlib.FieldTheory.IntermediateField.Algebraic` `Mathlib.FieldTheory.IntermediateField.ExtendRight` `Mathlib.FieldTheory.Minpoly.Field` `Mathlib.FieldTheory.Normal.Defs` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.LinearAlgebra.AnnihilatingPolynomial` `Mathlib.LinearAlgebra.Center` `Mathlib.LinearAlgebra.Charpoly.BaseChange` `Mathlib.LinearAlgebra.Charpoly.Basic` `Mathlib.LinearAlgebra.Charpoly.ToMatrix` `Mathlib.LinearAlgebra.Eigenspace.Minpoly` `Mathlib.LinearAlgebra.Eigenspace.Zero` `Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap` `Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly` `Mathlib.LinearAlgebra.SpecialLinearGroup` `Mathlib.LinearAlgebra.Transvection.Basic` `Mathlib.LinearAlgebra.Transvection` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.Niven` `Mathlib.RingTheory.Adjoin.PowerBasis` `Mathlib.RingTheory.Algebraic.Integral` `Mathlib.RingTheory.AlgebraicIndependent.Adjoin` `Mathlib.RingTheory.ClassGroup` `Mathlib.RingTheory.Conductor` `Mathlib.RingTheory.DedekindDomain.Basic` `Mathlib.RingTheory.DedekindDomain.Ideal.Basic` `Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.Ideal.GoingUp` `Mathlib.RingTheory.IntegralClosure.Algebra.Basic` `Mathlib.RingTheory.IntegralClosure.Algebra.Ideal` `Mathlib.RingTheory.IntegralClosure.IntegrallyClosed` `Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic` `Mathlib.RingTheory.Jacobson.Ring` `Mathlib.RingTheory.LocalProperties.IntegrallyClosed` `Mathlib.RingTheory.Localization.Integral` `Mathlib.RingTheory.NoetherNormalization` `Mathlib.RingTheory.Polynomial.RationalRoot` `Mathlib.RingTheory.PowerBasis` `Mathlib.RingTheory.RingHom.Integral` `Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup` `Mathlib.RingTheory.Valuation.Integral`	3
`Mathlib.FieldTheory.Minpoly.Finite` (new file)	1573

Declarations diff

+ FG.exists_span_finset_card_eq_spanFinrank
+ LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero
+ LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero
+ degree_le
+ natDegree_le
+ natDegree_le_spanFinrank
+ spanFinrank_subsingleton
+ spanRank_subsingleton
- LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul
- minpoly.degree_le
- minpoly.natDegree_le

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).

Copilot

Pull request overview

This PR generalizes degree bounds for minimal polynomials from finite-dimensional vector spaces to finite free modules, and correspondingly strengthens the Cayley–Hamilton-style existence statement to control the polynomial’s natDegree via spanFinrank.

Changes:

Add Mathlib.FieldTheory.Minpoly.Free with minpoly.natDegree_le / minpoly.degree_le for finite free algebras/modules.
Strengthen the Cayley–Hamilton auxiliary existence theorem for Module.Finite modules to produce a monic polynomial with natDegree = (⊤ : Submodule R M).spanFinrank, and thread this through downstream lemmas.
Introduce supporting API in SpanRank for extracting a generating Finset of cardinality spanFinrank, and update imports/usages accordingly.

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
Mathlib/RingTheory/Valuation/Minpoly.lean	Switch imports to the new minpoly degree-bound API (`Minpoly.Free`) and rely on the generalized bound.
Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean	Strengthen Cayley–Hamilton existence theorem with an explicit `natDegree = spanFinrank` conclusion; add deprecation alias and derived corollaries.
Mathlib/FieldTheory/Normal/Basic.lean	Adjust imports to pick up the new minpoly API (but currently drops a needed `Normal` definition import).
Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean	Import `Minpoly.Free` to access the generalized minpoly degree bound.
Mathlib/FieldTheory/Minpoly/Free.lean	New file: proves `minpoly.natDegree_le_spanFinrank`, then specializes to `Module.finrank` for finite free algebras.
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean	Remove the older `FiniteDimensional`-specific `minpoly.natDegree_le` / `minpoly.degree_le` lemmas in favor of the new general ones.
Mathlib/Analysis/Complex/Polynomial/Basic.lean	Update proof of `Irreducible.natDegree_le_two` to use the generalized `minpoly.natDegree_le`.
Mathlib/Algebra/Module/SpanRank.lean	Add API to extract a generating finset of size `spanFinrank`; add simp lemmas for subsingleton rings (currently with an instance issue).
Mathlib.lean	Export the new `Mathlib.FieldTheory.Minpoly.Free` module at the top level.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

mathlib-merge-conflicts · 2026-04-15T21:31:48Z

This pull request has conflicts, please merge master and resolve them.

…0/mathlib4 into generalise_natDegree_le

artie2000 · 2026-04-17T13:59:52Z

The context of this PR changed since #36421 got merged. It no longer generalises the statement of minpoly.natDegree_le, although it does move the proof earlier and prove a more general version of the result.

riccardobrasca · 2026-04-17T15:42:27Z

Can you update the PR description?

artie2000 · 2026-04-17T22:55:24Z

Can you update the PR description?

I already changed both the title and description to reflect the changed context. I've re-edited it now to hopefully be a little clearer.

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

riccardobrasca · 2026-04-19T10:01:57Z

Thanks!

bors d+

mathlib-bors · 2026-04-19T10:01:59Z

✌️ artie2000 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

artie2000 · 2026-04-19T17:49:27Z

thanks

bors r+

* Strengthen the statement of Cayley-Hamilton to bound the degree of the annihilating polynomial by the number of generators * Generalise `minpoly.natDegree_le` to non-free modules: `minpoly.natDegree_le_spanFinrank`

mathlib-bors · 2026-04-19T18:03:06Z

Build failed:

ci (staging) / Build

Fix if necessary, and then someone with permission can run bors r+ or bors retry.

Reformat comment for better readability.

artie2000 · 2026-04-19T18:31:59Z

bors retry

* Strengthen the statement of Cayley-Hamilton to bound the degree of the annihilating polynomial by the number of generators * Generalise `minpoly.natDegree_le` to non-free modules: `minpoly.natDegree_le_spanFinrank`

mathlib-bors · 2026-04-19T18:44:15Z

Pull request successfully merged into master.

Build succeeded:

initial commit

f0a25b3

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Apr 10, 2026

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Apr 10, 2026

artie2000 mentioned this pull request Apr 10, 2026

[Merged by Bors] - feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' #36421

Closed

artie2000 added 4 commits April 10, 2026 03:33

fix

1734e83

remove redundant line

a2b4ef5

Merge branch 'master' into generalise_natDegree_le

6181e21

min imports?

33b3f87

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Apr 11, 2026

Merge branch 'master' into generalise_natDegree_le

b465e62

riccardobrasca self-assigned this Apr 13, 2026

riccardobrasca requested a review from Copilot April 14, 2026 10:42

Copilot started reviewing on behalf of riccardobrasca April 14, 2026 10:43 View session

riccardobrasca reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/SpanRank.lean Outdated

Comment thread Mathlib/FieldTheory/Minpoly/Free.lean Outdated

Comment thread Mathlib/FieldTheory/Minpoly/Free.lean Outdated

Comment thread Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean Outdated

Copilot AI reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/SpanRank.lean Outdated

Comment thread Mathlib/Algebra/Module/SpanRank.lean Outdated

Comment thread Mathlib/FieldTheory/Normal/Basic.lean Outdated

Comment thread Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean

artie2000 added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 14, 2026

artie2000 added 6 commits April 14, 2026 23:47

review comments

ee9038c

lint

211da66

update docs

2ca250b

small golf

583d722

swich to nontriviality from simp

b94c63d

inline instance

93a285d

artie2000 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 14, 2026

artie2000 requested a review from riccardobrasca April 14, 2026 23:06

Merge branch 'master' into generalise_natDegree_le

e56157f

mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 15, 2026

Merge branch 'master' into generalise_natDegree_le

1f7f6ca

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 17, 2026

artie2000 added 2 commits April 17, 2026 14:28

update

62b97ce

clean up

a487f95

artie2000 changed the title ~~feat: generalise degree bound for minimal polynomial~~ feat: strengthen Cayley-Hamilton Apr 17, 2026

artie2000 added 3 commits April 17, 2026 14:44

Merge branch 'master' into generalise_natDegree_le

3e52823

fix imports

c00f87a

Merge branch 'generalise_natDegree_le' of https://github.com/artie200…

6ced952

…0/mathlib4 into generalise_natDegree_le

riccardobrasca reviewed Apr 18, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Module/SpanRank.lean

Comment thread Mathlib/FieldTheory/Normal/Basic.lean

Comment thread Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean Outdated

Comment thread Mathlib/FieldTheory/Minpoly/Finite.lean Outdated

Update Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean

84ee0bb

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 19, 2026

Update Mathlib/FieldTheory/Minpoly/Finite.lean

423ad87

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

artie2000 added 2 commits April 19, 2026 19:30

Merge branch 'master' into generalise_natDegree_le

e34a00a

lint

c513243

Reformat comment for better readability.

mathlib-bors bot changed the title ~~feat: strengthen Cayley-Hamilton~~ [Merged by Bors] - feat: strengthen Cayley-Hamilton Apr 19, 2026

mathlib-bors bot closed this Apr 19, 2026

Conversation

artie2000 commented Apr 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2c53994ec0

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Apr 15, 2026

Uh oh!

artie2000 commented Apr 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

riccardobrasca commented Apr 17, 2026

Uh oh!

artie2000 commented Apr 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Apr 19, 2026

Uh oh!

mathlib-bors bot commented Apr 19, 2026

Uh oh!

artie2000 commented Apr 19, 2026

Uh oh!

mathlib-bors bot commented Apr 19, 2026

Uh oh!

artie2000 commented Apr 19, 2026

Uh oh!

mathlib-bors bot commented Apr 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

artie2000 commented Apr 10, 2026 •

edited

Loading

github-actions bot commented Apr 10, 2026 •

edited

Loading

artie2000 commented Apr 17, 2026 •

edited

Loading

artie2000 commented Apr 17, 2026 •

edited

Loading