Commit 2024-01-25 14:36 8853442f

View on Github →

feat: define semisimple linear endomorphisms (#9825)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Map.lean

added theorem Submodule.comap_neg

Modified Mathlib/Data/Polynomial/Module.lean

added theorem Module.AEval.injective_comapSubmodule

added theorem Module.AEval.range_comapSubmodule

Modified Mathlib/GroupTheory/Nilpotent.lean

Created Mathlib/LinearAlgebra/Semisimple.lean

added theorem Module.End.IsSemisimple_smul

added theorem Module.End.IsSemisimple_smul_iff

added theorem Module.End.eq_zero_of_isNilpotent_isSemisimple

added theorem Module.End.isSemisimple_id

added theorem Module.End.isSemisimple_iff

added theorem Module.End.isSemisimple_neg

added theorem Module.End.isSemisimple_zero

Modified Mathlib/Order/CompleteSublattice.lean

added theorem CompleteLatticeHom.range_coe

added theorem CompleteSublattice.coe_copy

added theorem CompleteSublattice.copy_eq

added theorem CompleteSublattice.isComplemented_iff

Modified Mathlib/Order/Disjoint.lean

added theorem Codisjoint.ne_bot_of_ne_top'

added theorem Codisjoint.ne_bot_of_ne_top

Modified Mathlib/Order/Hom/Lattice.lean

added def orderEmbeddingOfInjective

Modified Mathlib/Order/Hom/Set.lean

Modified Mathlib/RingTheory/Nilpotent.lean

added theorem eq_zero_of_nilpotencyClass_eq_one

added theorem isNilpotent_of_pos_nilpotencyClass

added theorem isNilpotent_of_subsingleton

added theorem nilpotencyClass_eq_one

added theorem nilpotencyClass_eq_succ_iff

added theorem nilpotencyClass_eq_zero_of_subsingleton

added theorem nilpotencyClass_zero

added theorem pos_nilpotencyClass_iff

added theorem pow_nilpotencyClass

added theorem pow_pred_nilpotencyClass