Commit 2024-02-01 15:16 be2a49b5

View on Github →

feat: a linear endomorphism that is a root of a squarefree polynomial is semisimple (#10128) The main result is Module.End.isSemisimple_of_squarefree_aeval_eq_zero

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Associated.lean

added theorem prime_mul_iff

added theorem prime_pow_iff

Modified Mathlib/Analysis/Calculus/Taylor.lean

Modified Mathlib/Data/Polynomial/Derivation.lean

Renamed Mathlib/Data/Polynomial/Module.lean to Mathlib/Data/Polynomial/Module/Basic.lean

Created Mathlib/Data/Polynomial/Module/FiniteDimensional.lean

added theorem Module.AEval.isTorsion_of_aeval_eq_zero

added theorem Module.AEval.isTorsion_of_finiteDimensional

Modified Mathlib/LinearAlgebra/Semisimple.lean

modified theorem Module.End.IsSemisimple_smul

added theorem Module.End.isSemisimple_of_squarefree_aeval_eq_zero

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

added theorem Ideal.factors_span_eq

added theorem Ideal.prime_generator_of_prime

added theorem Ideal.prime_span_singleton_iff

added theorem Ideal.squarefree_span_singleton

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/RingTheory/FiniteType.lean

Modified Mathlib/RingTheory/Ideal/Basic.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

added theorem Submodule.IsPrincipal.associated_generator_span_self

Modified Mathlib/RingTheory/SimpleModule.lean

deleted theorem isSemisimpleModule_biSup_of_IsSemisimpleModule_submodule

added theorem isSemisimpleModule_biSup_of_isSemisimpleModule_submodule

deleted theorem isSemisimpleModule_of_IsSemisimpleModule_submodule'

deleted theorem isSemisimpleModule_of_IsSemisimpleModule_submodule

added theorem isSemisimpleModule_of_isSemisimpleModule_submodule'

added theorem isSemisimpleModule_of_isSemisimpleModule_submodule