Commit 2024-04-20 11:56 4421fe03

View on Github →

feat(Algebra/Lie/Rank): the rank of a Lie algebra, and regular elements (#10628) We define the rank of a finite dimensional Lie algebra, and prove the existence of regular elements over sufficiently large base fields.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/Rank.lean

added theorem LieAlgebra.exists_isRegular

added theorem LieAlgebra.exists_isRegular_of_finrank_le_card

added theorem LieAlgebra.isRegular_def

added theorem LieAlgebra.isRegular_iff_coeff_polyCharpoly_rank_ne_zero

added theorem LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank

added theorem LieAlgebra.polyCharpoly_coeff_rank_ne_zero

added theorem LieAlgebra.rank_eq_natTrailingDegree

added theorem LieAlgebra.rank_le_card

added theorem LieAlgebra.rank_le_finrank

added theorem LieAlgebra.rank_le_natTrailingDegree_charpoly_ad

added def LieModule.IsRegular

added theorem LieModule.exists_isRegular

added theorem LieModule.exists_isRegular_of_finrank_le_card

added theorem LieModule.isRegular_def

added theorem LieModule.isRegular_iff_coeff_polyCharpoly_rank_ne_zero

added theorem LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank

added theorem LieModule.polyCharpoly_coeff_rank_ne_zero

added def LieModule.rank

added theorem LieModule.rank_eq_natTrailingDegree

added theorem LieModule.rank_le_card

added theorem LieModule.rank_le_finrank

added theorem LieModule.rank_le_natTrailingDegree_charpoly_ad

Modified Mathlib/Algebra/Module/LinearMap/Polynomial.lean

added def LinearMap.IsNilRegular

added theorem LinearMap.exists_isNilRegular

added theorem LinearMap.exists_isNilRegular_of_finrank_le_card

added theorem LinearMap.isNilRegular_def

added theorem LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero

added theorem LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank

added def LinearMap.nilRank

added def LinearMap.nilRankAux

added theorem LinearMap.nilRankAux_basis_indep

added theorem LinearMap.nilRankAux_le

added theorem LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree

added theorem LinearMap.nilRank_le_card

added theorem LinearMap.nilRank_le_finrank

added theorem LinearMap.nilRank_le_natTrailingDegree_charpoly

added theorem LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis

added theorem LinearMap.polyCharpoly_coeff_eq_zero_of_basis

modified theorem LinearMap.polyCharpoly_coeff_isHomogeneous

added theorem LinearMap.polyCharpoly_coeff_nilRankAux_ne_zero

added theorem LinearMap.polyCharpoly_coeff_nilRank_ne_zero

modified theorem LinearMap.polyCharpoly_natDegree

modified theorem LinearMap.toMvPolynomial_add

added theorem LinearMap.toMvPolynomial_id

modified theorem LinearMap.toMvPolynomial_zero

modified theorem Matrix.toMvPolynomial_add

added theorem Matrix.toMvPolynomial_one

modified theorem Matrix.toMvPolynomial_zero

Modified docs/references.bib