Commit 2024-10-26 13:47 158ff637

View on Github →

chore(LinearAlgebra): rename unifEigenspace to genEigenspace (#18251)

Estimated changes

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

added def Module.End.genEigenrange

added theorem Module.End.genEigenrange_nat

modified def Module.End.genEigenspace

added theorem Module.End.genEigenspace_directed

added theorem Module.End.genEigenspace_div

added theorem Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le

added theorem Module.End.genEigenspace_eq_iSup_genEigenspace_nat

added theorem Module.End.genEigenspace_inf_le_add

modified theorem Module.End.genEigenspace_le_genEigenspace_finrank

added theorem Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex

added theorem Module.End.genEigenspace_le_smul

added theorem Module.End.genEigenspace_nat

added theorem Module.End.genEigenspace_one

modified theorem Module.End.genEigenspace_restrict

added theorem Module.End.genEigenspace_top

added theorem Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex

modified theorem Module.End.genEigenspace_zero

added theorem Module.End.genEigenspace_zero_nat

modified theorem Module.End.independent_genEigenspace

added theorem Module.End.independent_iSup_genEigenspace

deleted theorem Module.End.independent_unifEigenspace

modified theorem Module.End.injOn_genEigenspace

added theorem Module.End.injOn_iSup_genEigenspace

deleted theorem Module.End.injOn_unifEigenspace

added theorem Module.End.isNilpotent_restrict_genEigenspace_nat

added theorem Module.End.isNilpotent_restrict_genEigenspace_top

deleted theorem Module.End.isNilpotent_restrict_unifEigenspace_nat

deleted theorem Module.End.isNilpotent_restrict_unifEigenspace_top

added theorem Module.End.map_add_of_iInf_iSup_genEigenspace_ne_bot_of_commute

deleted theorem Module.End.map_add_of_iInf_unifEigenspace_ne_bot_of_commute

added theorem Module.End.map_smul_of_iInf_iSup_genEigenspace_ne_bot

deleted theorem Module.End.map_smul_of_iInf_unifEigenspace_ne_bot

modified theorem Module.End.mapsTo_genEigenspace_of_comm

deleted theorem Module.End.mapsTo_unifEigenspace_of_comm

modified theorem Module.End.mem_genEigenspace

added theorem Module.End.mem_genEigenspace_nat

added theorem Module.End.mem_genEigenspace_one

added theorem Module.End.mem_genEigenspace_top

added theorem Module.End.mem_genEigenspace_zero

deleted theorem Module.End.mem_unifEigenspace

deleted theorem Module.End.mem_unifEigenspace_nat

deleted theorem Module.End.mem_unifEigenspace_one

deleted theorem Module.End.mem_unifEigenspace_top

deleted theorem Module.End.mem_unifEigenspace_zero

deleted def Module.End.unifEigenrange

deleted theorem Module.End.unifEigenrange_nat

deleted def Module.End.unifEigenspace

deleted theorem Module.End.unifEigenspace_directed

deleted theorem Module.End.unifEigenspace_div

deleted theorem Module.End.unifEigenspace_eq_iSup_unifEigenspace_nat

deleted theorem Module.End.unifEigenspace_eq_unifEigenspace_finrank_of_le

deleted theorem Module.End.unifEigenspace_eq_unifEigenspace_maxUnifEigenspaceIndex_of_le

deleted theorem Module.End.unifEigenspace_inf_le_add

deleted theorem Module.End.unifEigenspace_le_smul

deleted theorem Module.End.unifEigenspace_le_unifEigenspace_finrank

deleted theorem Module.End.unifEigenspace_le_unifEigenspace_maxUnifEigenspaceIndex

deleted theorem Module.End.unifEigenspace_nat

deleted theorem Module.End.unifEigenspace_one

deleted theorem Module.End.unifEigenspace_restrict

deleted theorem Module.End.unifEigenspace_top

deleted theorem Module.End.unifEigenspace_top_eq_maxUnifEigenspaceIndex

deleted theorem Module.End.unifEigenspace_zero

deleted theorem Module.End.unifEigenspace_zero_nat

modified theorem Submodule.inf_genEigenspace

deleted theorem Submodule.inf_unifEigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Pi.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean

deleted theorem Module.End.IsFinitelySemisimple.unifEigenspace_eq_eigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

added theorem Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top

deleted theorem Module.End.exists_hasEigenvalue_of_unifEigenspace_eq_top

added theorem Module.End.genEigenspace_restrict_eq_top

deleted theorem Module.End.unifEigenspace_restrict_eq_top

modified theorem Submodule.eq_iSup_inf_genEigenspace

deleted theorem Submodule.eq_iSup_inf_unifEigenspace

modified theorem Submodule.inf_iSup_genEigenspace

deleted theorem Submodule.inf_iSup_unifEigenspace

Modified Mathlib/LinearAlgebra/Eigenspace/Zero.lean