Commit 2024-10-25 20:58 99c058ff

View on Github →

chore(LinearAlgebra): use maxGenEigenspace instead of iSup over genEigenspace (#18037)

Estimated changes

Modified Mathlib/Algebra/Lie/TraceForm.lean

Modified Mathlib/Algebra/Lie/Weights/Basic.lean

Modified Mathlib/Algebra/Lie/Weights/Linear.lean

Modified Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

deleted theorem Module.End.iSup_genEigenspace_eq_genEigenspace_finrank

added theorem Module.End.independent_unifEigenspace

added theorem Module.End.injOn_maxGenEigenspace

added theorem Module.End.injOn_unifEigenspace

added theorem Module.End.map_add_of_iInf_unifEigenspace_ne_bot_of_commute

added theorem Module.End.map_smul_of_iInf_unifEigenspace_ne_bot

added theorem Module.End.maxGenEigenspace_eq_genEigenspace_finrank

added theorem Module.End.unifEigenspace_inf_le_add

added theorem Module.End.unifEigenspace_le_smul

added theorem Module.End.unifEigenspace_restrict

added theorem Submodule.inf_unifEigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Pi.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean

added theorem Module.End.IsFinitelySemisimple.unifEigenspace_eq_eigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

added theorem Module.End.exists_hasEigenvalue_of_unifEigenspace_eq_top

added theorem Module.End.iSup_maxGenEigenspace_eq_top

added theorem Module.End.unifEigenspace_restrict_eq_top

added theorem Submodule.eq_iSup_inf_unifEigenspace

added theorem Submodule.inf_iSup_unifEigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Zero.lean

Modified Mathlib/Order/SupIndep.lean

added theorem Finset.supIndep_antimono_fun