Commit 2025-08-14 04:35 606d5971

View on Github →

feat(RingTheory): semisimple Wedderburn–Artin existence (#24192)

Estimated changes

Modified Mathlib/Algebra/Algebra/Pi.lean

modified def AlgEquiv.piCongrLeft'

added def AlgEquiv.piMulOpposite

Modified Mathlib/Algebra/Ring/Equiv.lean

added def RingEquiv.piMulOpposite

Modified Mathlib/LinearAlgebra/DFinsupp.lean

added theorem iSupIndep.linearEquiv_symm_apply

Modified Mathlib/Order/CompleteSublattice.lean

added theorem CompleteSublattice.bot_mem

added theorem CompleteSublattice.coe_iInf

added theorem CompleteSublattice.coe_iSup

added theorem CompleteSublattice.top_mem

Modified Mathlib/RingTheory/SimpleModule/Basic.lean

modified theorem IsSemisimpleModule.eq_bot_or_exists_simple_le

Modified Mathlib/RingTheory/SimpleModule/IsAlgClosed.lean

added theorem IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed

modified theorem IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed

Modified Mathlib/RingTheory/SimpleModule/Isotypic.lean

added def GaloisCoinsertion.setIsotypicComponents

added theorem IsIsotypic.submodule_linearEquiv_fun

added theorem LinearEquiv.isotypicComponent_eq

added theorem LinearMap.le_comap_isotypicComponent

added def OrderIso.setIsotypicComponents

added theorem Submodule.IsFullyInvariant.of_mem_isotypicComponents

added theorem Submodule.map_le_isotypicComponent

added theorem bot_lt_isotypicComponents

added theorem eq_isotypicComponent_iff

added theorem eq_isotypicComponent_of_le

added def fullyInvariantSubmodule

added theorem isFullyInvariant_iff_le_imp_isotypicComponent_le

added theorem isFullyInvariant_iff_sSup_isotypicComponents

deleted theorem isFullyInvariant_isotypicComponent

modified theorem isIsotypic_iff_isFullyInvariant_imp_bot_or_top

added def isotypicComponents

added theorem le_isotypicComponent_iff

added theorem mem_fullyInvariantSubmodule_iff

added theorem mem_isotypicComponents_iff

added theorem sSupIndep_isotypicComponents

added theorem sSup_isotypicComponents

Modified Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

added theorem IsSemisimpleModule.exists_end_algEquiv

added theorem IsSemisimpleModule.exists_end_ringEquiv

added theorem IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing

added theorem IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite

added theorem IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite

added theorem IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing

added theorem IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite

Modified docs/1000.yaml