Commit 2025-05-15 14:58 3a7e90ab

View on Github →

feat(RingTheory): isotypic API and simple Wedderburn–Artin existence (#23963) A replacement of #23583 with more meaningful intermediate results.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/SimpleModule/Basic.lean

added theorem IsSemisimpleModule.exists_linearEquiv_dfinsupp

added theorem IsSemisimpleModule.exists_linearEquiv_fin_dfinsupp

added theorem IsSemisimpleModule.extension_property

modified theorem IsSimpleModule.congr

added theorem LinearEquiv.isSemisimpleModule_iff

added theorem LinearEquiv.isSimpleModule_iff

added theorem LinearMap.linearEquiv_of_ne_zero

Created Mathlib/RingTheory/SimpleModule/IsAlgClosed.lean

added theorem IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed

Created Mathlib/RingTheory/SimpleModule/Isotypic.lean

added theorem IsIsotypic.linearEquiv_finsupp

added theorem IsIsotypic.linearEquiv_fun

added theorem IsIsotypic.of_injective

added theorem IsIsotypic.of_subsingleton

added def IsIsotypic

added theorem IsIsotypicOfType.isIsotypic

added theorem IsIsotypicOfType.linearEquiv_finsupp

added theorem IsIsotypicOfType.linearEquiv_fun

added theorem IsIsotypicOfType.of_injective

added theorem IsIsotypicOfType.of_isSimpleModule

added theorem IsIsotypicOfType.of_isotypicComponent_eq_top

added theorem IsIsotypicOfType.of_linearEquiv_type

added theorem IsIsotypicOfType.of_subsingleton

added def IsIsotypicOfType

added theorem LinearEquiv.isIsotypicOfType_iff

added theorem LinearEquiv.isIsotypicOfType_iff_type

added theorem LinearEquiv.isIsotypic_iff

added def Submodule.IsFullyInvariant

added theorem Submodule.le_isotypicComponent

added theorem Submodule.le_linearEquiv_of_le_sSup

added theorem Submodule.le_linearEquiv_of_sSup_eq_top

added theorem Submodule.linearEquiv_of_le_sSup

added theorem Submodule.linearEquiv_of_sSup_eq_top

added theorem bot_lt_isotypicComponent

added theorem isFullyInvariant_iff_isTwoSided

added theorem isFullyInvariant_isotypicComponent

added theorem isIsotypicOfType_submodule_iff

added theorem isIsotypic_iff_isFullyInvariant_imp_bot_or_top

added theorem isIsotypic_submodule_iff

added def isotypicComponent

added theorem isotypicComponent_eq_top_iff

Created Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

added theorem IsSimpleRing.exists_algEquiv_matrix_divisionRing

added theorem IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite

added theorem IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite

added theorem IsSimpleRing.exists_ringEquiv_matrix_divisionRing

added theorem IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite

added theorem IsSimpleRing.isIsotypic

added theorem IsSimpleRing.isSemisimpleRing_iff_isArtinianRing

added theorem IsSimpleRing.tfae

added theorem isSimpleRing_isArtinianRing_iff