Commit 2023-04-06 14:19 c6bb7e60

View on Github →

feat: port RingTheory.SimpleModule (#3267)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/SimpleModule.lean

added theorem IsSemisimpleModule.supₛ_simples_eq_top

added theorem IsSimpleModule.congr

added theorem IsSimpleModule.isAtom

added theorem IsSimpleModule.nontrivial

added def JordanHolderModule.Iso

added theorem JordanHolderModule.iso_symm

added theorem JordanHolderModule.iso_trans

added theorem JordanHolderModule.second_iso

added theorem LinearMap.bijective_of_ne_zero

added theorem LinearMap.bijective_or_eq_zero

added theorem LinearMap.injective_of_ne_zero

added theorem LinearMap.injective_or_eq_zero

added theorem LinearMap.isCoatom_ker_of_surjective

added theorem LinearMap.surjective_of_ne_zero

added theorem LinearMap.surjective_or_eq_zero

added theorem covby_iff_quot_is_simple

added theorem isSimpleModule_iff_isAtom

added theorem isSimpleModule_iff_isCoatom

added theorem is_semisimple_iff_top_eq_supₛ_simples

added theorem is_semisimple_of_supₛ_simples_eq_top