Commit 2024-10-07 14:27 5017a681

View on Github →

refactor(LinearAlgebra/Eigenspace): unified definition of (max(gen)?)?Eigenspace (#16025)

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

Modified Mathlib/Algebra/Lie/TraceForm.lean

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

Modified Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

deleted def Module.End.Eigenvalues.val

deleted def Module.End.Eigenvalues

deleted def Module.End.HasEigenvalue

deleted def Module.End.HasEigenvector

deleted def Module.End.HasGenEigenvalue

deleted def Module.End.HasGenEigenvector

added theorem Module.End.HasUnifEigenvalue.exists_hasUnifEigenvector

added theorem Module.End.HasUnifEigenvalue.exp_ne_zero

added theorem Module.End.HasUnifEigenvalue.isNilpotent_of_isNilpotent

added theorem Module.End.HasUnifEigenvalue.le

added theorem Module.End.HasUnifEigenvalue.lt

added theorem Module.End.HasUnifEigenvalue.mem_spectrum

added theorem Module.End.HasUnifEigenvalue.pow

added def Module.End.HasUnifEigenvalue

added theorem Module.End.HasUnifEigenvector.apply_eq_smul

added theorem Module.End.HasUnifEigenvector.hasUnifEigenvalue

added theorem Module.End.HasUnifEigenvector.pow_apply

added def Module.End.HasUnifEigenvector

added def Module.End.UnifEigenvalues.val

added def Module.End.UnifEigenvalues

added theorem Module.End.disjoint_unifEigenspace

deleted def Module.End.eigenspace

modified theorem Module.End.eigenspace_def

modified theorem Module.End.eigenspace_zero

deleted def Module.End.genEigenrange

modified theorem Module.End.genEigenrange_def

modified theorem Module.End.hasEigenvalue_iff

modified theorem Module.End.hasGenEigenvalue_iff

added theorem Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one

added theorem Module.End.hasUnifEigenvalue_iff_mem_spectrum

added theorem Module.End.iSup_genEigenspace_eq

added theorem Module.End.independent_maxGenEigenspace

added theorem Module.End.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap

added theorem Module.End.isNilpotent_restrict_unifEigenspace_nat

added theorem Module.End.isNilpotent_restrict_unifEigenspace_top

added theorem Module.End.mapsTo_maxGenEigenspace_of_comm

added theorem Module.End.mapsTo_unifEigenspace_of_comm

deleted def Module.End.maxGenEigenspace

modified theorem Module.End.maxGenEigenspace_eq

added theorem Module.End.maxUnifEigenspaceIndex_le_finrank

modified theorem Module.End.mem_eigenspace_iff

added theorem Module.End.mem_unifEigenspace

added theorem Module.End.mem_unifEigenspace_nat

added theorem Module.End.mem_unifEigenspace_one

added theorem Module.End.mem_unifEigenspace_top

added theorem Module.End.mem_unifEigenspace_zero

added def Module.End.unifEigenrange

added theorem Module.End.unifEigenrange_nat

added def Module.End.unifEigenspace

added theorem Module.End.unifEigenspace_directed

added theorem Module.End.unifEigenspace_div

added theorem Module.End.unifEigenspace_eq_iSup_unifEigenspace_nat

added theorem Module.End.unifEigenspace_eq_unifEigenspace_finrank_of_le

added theorem Module.End.unifEigenspace_eq_unifEigenspace_maxUnifEigenspaceIndex_of_le

added theorem Module.End.unifEigenspace_le_unifEigenspace_finrank

added theorem Module.End.unifEigenspace_le_unifEigenspace_maxUnifEigenspaceIndex

added theorem Module.End.unifEigenspace_nat

added theorem Module.End.unifEigenspace_one

added theorem Module.End.unifEigenspace_top

added theorem Module.End.unifEigenspace_top_eq_maxUnifEigenspaceIndex

added theorem Module.End.unifEigenspace_zero

added theorem Module.End.unifEigenspace_zero_nat

Modified Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

Modified Mathlib/Order/Hom/Basic.lean

added def WithBot.coeOrderHom

added def WithTop.coeOrderHom

Modified Mathlib/RingTheory/Nilpotent/Lemmas.lean

modified theorem Module.End.isNilpotent.restrict

added theorem Module.End.isNilpotent_restrict_of_le