Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-02-07 15:18
8857f4e2
View on Github →
feat: add proof of Jordan-Chevalley-Dunford decomposition (
#10295
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Group/Units.lean
added
theorem
isUnit_of_mul_eq_one_right
Modified
Mathlib/Data/Polynomial/AlgebraMap.lean
added
theorem
Polynomial.aeval_mem_adjoin_singleton
added
theorem
Polynomial.coe_aeval_mk_apply
Created
Mathlib/LinearAlgebra/JordanChevalley.lean
added
theorem
Module.End.exists_isNilpotent_isSemisimple
added
theorem
Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow
Modified
docs/undergrad.yaml