Commit 2026-04-19 18:32 d2962c4e

View on Github →

feat: strengthen Cayley-Hamilton (#37872)

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/SpanRank.lean

added theorem Submodule.FG.exists_span_finset_card_eq_spanFinrank

added theorem Submodule.spanFinrank_subsingleton

added theorem Submodule.spanRank_subsingleton

Modified Mathlib/Analysis/Complex/Polynomial/Basic.lean

Created Mathlib/FieldTheory/Minpoly/Finite.lean

added theorem minpoly.degree_le

added theorem minpoly.natDegree_le

added theorem minpoly.natDegree_le_spanFinrank

Modified Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Modified Mathlib/FieldTheory/Normal/Basic.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Exponent.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

deleted theorem minpoly.degree_le

deleted theorem minpoly.natDegree_le

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

deleted theorem LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul

added theorem LinearMap.exists_monic_and_natDegree_eq_and_aeval_eq_zero

added theorem LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/Valuation/Minpoly.lean

Modified docs/references.bib