Commit 2023-10-10 23:14 b400da17

View on Github →

feat: improve API for Fitting decomposition of a linear endomorphism (#7487) Especially the new lemma LinearMap.eventually_isCompl_ker_pow_range_pow

Estimated changes

Modified Mathlib/Algebra/Lie/Weights.lean

deleted theorem LieModule.exists_coe_posFittingCompOf_eq_of_isArtinian

Modified Mathlib/RingTheory/Artinian.lean

added theorem IsArtinian.eventuallyConst_of_isArtinian

deleted theorem IsArtinian.exists_endomorphism_iterate_ker_sup_range_eq_top

added theorem LinearMap.eventually_codisjoint_ker_pow_range_pow

added theorem LinearMap.eventually_iInf_range_pow_eq

added theorem LinearMap.eventually_isCompl_ker_pow_range_pow

deleted theorem LinearMap.exists_range_pow_eq_iInf

added theorem LinearMap.isCompl_iSup_ker_pow_iInf_range_pow

Modified Mathlib/RingTheory/Noetherian.lean

modified theorem IsNoetherian.bijective_of_surjective_endomorphism

modified theorem IsNoetherian.disjoint_partialSups_eventually_bot

deleted theorem IsNoetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot

modified theorem IsNoetherian.injective_of_surjective_endomorphism

added theorem LinearMap.eventually_disjoint_ker_pow_range_pow

added theorem LinearMap.eventually_iSup_ker_pow_eq

added theorem eventuallyConst_of_isNoetherian

modified theorem finite_of_linearIndependent

modified theorem isNoetherian_of_range_eq_ker