Commit 2024-05-21 19:30 36288957

View on Github →

chore(Algebra,LinearAlgebra): shorten names of generalizedEigenspace and maximalGeneralizedEigenspace (#13078) This commit is generated using rg -l generalizedEigenspace | xargs sed -i 's/generalizedEigenspace/genEigenspace/g' rg -l maximalGeneralizedEigenspace | xargs sed -i 's/maximalGeneralizedEigenspace/maxGenEigenspace/g' rg -l HasGeneralizedEigen | xargs sed -i 's/HasGeneralizedEigen/HasGenEigen/g' rg -l generalizedEigenrange | xargs sed -i 's/generalizedEigenrange/genEigenrange/g' rg -l hasGeneralizedEigen | xargs sed -i 's/hasGeneralizedEigen/hasGenEigen/g' The upshot is many shorter lemma names.

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

Modified Mathlib/Algebra/Lie/EngelSubalgebra.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

Modified Mathlib/Algebra/Lie/Rank.lean

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

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

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

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added def Module.End.HasGenEigenvalue

added def Module.End.HasGenEigenvector

deleted def Module.End.HasGeneralizedEigenvalue

deleted def Module.End.HasGeneralizedEigenvector

added theorem Module.End.disjoint_genEigenspace

deleted theorem Module.End.disjoint_generalizedEigenspace

added theorem Module.End.disjoint_iSup_genEigenspace

deleted theorem Module.End.disjoint_iSup_generalizedEigenspace

added theorem Module.End.eigenspace_le_genEigenspace

deleted theorem Module.End.eigenspace_le_generalizedEigenspace

added theorem Module.End.exp_ne_zero_of_hasGenEigenvalue

deleted theorem Module.End.exp_ne_zero_of_hasGeneralizedEigenvalue

added def Module.End.genEigenrange

added def Module.End.genEigenspace

added theorem Module.End.genEigenspace_eq_genEigenspace_finrank_of_le

added theorem Module.End.genEigenspace_le_genEigenspace_finrank

added theorem Module.End.genEigenspace_le_maximal

added theorem Module.End.genEigenspace_restrict

added theorem Module.End.genEigenspace_zero

deleted def Module.End.generalizedEigenrange

deleted def Module.End.generalizedEigenspace

deleted theorem Module.End.generalizedEigenspace_eq_generalizedEigenspace_finrank_of_le

deleted theorem Module.End.generalizedEigenspace_le_generalizedEigenspace_finrank

deleted theorem Module.End.generalizedEigenspace_le_maximal

deleted theorem Module.End.generalizedEigenspace_restrict

deleted theorem Module.End.generalizedEigenspace_zero

added theorem Module.End.hasEigenvalue_of_hasGenEigenvalue

deleted theorem Module.End.hasEigenvalue_of_hasGeneralizedEigenvalue

added theorem Module.End.hasGenEigenvalue_iff_hasEigenvalue

added theorem Module.End.hasGenEigenvalue_of_hasEigenvalue

added theorem Module.End.hasGenEigenvalue_of_hasGenEigenvalue_of_le

deleted theorem Module.End.hasGeneralizedEigenvalue_iff_hasEigenvalue

deleted theorem Module.End.hasGeneralizedEigenvalue_of_hasEigenvalue

deleted theorem Module.End.hasGeneralizedEigenvalue_of_hasGeneralizedEigenvalue_of_le

added theorem Module.End.iSup_genEigenspace_eq_genEigenspace_finrank

added theorem Module.End.iSup_genEigenspace_inf_le_add

added theorem Module.End.iSup_genEigenspace_le_smul

deleted theorem Module.End.iSup_generalizedEigenspace_eq_generalizedEigenspace_finrank

deleted theorem Module.End.iSup_generalizedEigenspace_inf_le_add

deleted theorem Module.End.iSup_generalizedEigenspace_le_smul

added theorem Module.End.independent_genEigenspace

deleted theorem Module.End.independent_generalizedEigenspace

added theorem Module.End.injOn_genEigenspace

deleted theorem Module.End.injOn_generalizedEigenspace

added theorem Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute

deleted theorem Module.End.map_add_of_iInf_generalizedEigenspace_ne_bot_of_commute

added theorem Module.End.map_genEigenrange_le

deleted theorem Module.End.map_generalizedEigenrange_le

added theorem Module.End.map_smul_of_iInf_genEigenspace_ne_bot

deleted theorem Module.End.map_smul_of_iInf_generalizedEigenspace_ne_bot

added theorem Module.End.mapsTo_genEigenspace_of_comm

deleted theorem Module.End.mapsTo_generalizedEigenspace_of_comm

added theorem Module.End.mapsTo_iSup_genEigenspace_of_comm

deleted theorem Module.End.mapsTo_iSup_generalizedEigenspace_of_comm

added def Module.End.maxGenEigenspace

added theorem Module.End.maxGenEigenspace_eq

deleted def Module.End.maximalGeneralizedEigenspace

deleted theorem Module.End.maximalGeneralizedEigenspace_eq

added theorem Module.End.mem_genEigenspace

deleted theorem Module.End.mem_generalizedEigenspace

added theorem Module.End.mem_maxGenEigenspace

deleted theorem Module.End.mem_maximalGeneralizedEigenspace

added theorem Module.End.pos_finrank_genEigenspace_of_hasEigenvalue

deleted theorem Module.End.pos_finrank_generalizedEigenspace_of_hasEigenvalue

added theorem Submodule.inf_genEigenspace

deleted theorem Submodule.inf_generalizedEigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean

added theorem Module.End.IsSemisimple.genEigenspace_eq_eigenspace

deleted theorem Module.End.IsSemisimple.generalizedEigenspace_eq_eigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

added theorem Module.End.iSup_genEigenspace_eq_top

added theorem Module.End.iSup_genEigenspace_restrict_eq_top

deleted theorem Module.End.iSup_generalizedEigenspace_eq_top

deleted theorem Module.End.iSup_generalizedEigenspace_restrict_eq_top

added theorem Submodule.eq_iSup_inf_genEigenspace

deleted theorem Submodule.eq_iSup_inf_generalizedEigenspace

added theorem Submodule.inf_iSup_genEigenspace

deleted theorem Submodule.inf_iSup_generalizedEigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Zero.lean

added theorem LinearMap.finrank_maxGenEigenspace

deleted theorem LinearMap.finrank_maximalGeneralizedEigenspace

Modified docs/undergrad.yaml