Commit 2025-08-05 16:35 e074407c

View on Github →

feat: basic linear algebra lemmas about matrices (#27605) These came up in the proof that the Geck Construction yields semisimple Lie algebras. I am splitting them into their own PR to simplify review.

Estimated changes

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

Modified Mathlib/Data/Matrix/Block.lean

added theorem Matrix.fromBlocks_diagonal_pow

Modified Mathlib/Data/Matrix/Diagonal.lean

added theorem Matrix.diagonal_one'

Modified Mathlib/Data/Matrix/Mul.lean

added theorem Matrix.commute_diagonal

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

added theorem Submodule.eq_top_iff_forall_basis_mem

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.eigenspace_le_maxGenEigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

added theorem Matrix.iSup_eigenspace_toLin'_diagonal_eq_top

added theorem Matrix.iSup_eigenspace_toLin_diagonal_eq_top

added theorem Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace

added theorem Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace

modified theorem spectrum_diagonal

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem Matrix.toLin'_pow

added theorem Matrix.toLin_apply_eq_zero_iff

added theorem Matrix.toLin_pow

Modified Mathlib/LinearAlgebra/Pi.lean

added theorem Pi.mem_span_range_single_inl_iff