Commit 2025-05-01 06:42 3c296322

View on Github →

feat: preliminaries for Wedderburn–Artin (#24119)

Estimated changes

Modified Mathlib/Algebra/Algebra/Opposite.lean

added def AlgEquiv.moduleEndSelf

added def AlgEquiv.moduleEndSelfOp

Modified Mathlib/Algebra/Azumaya/Basic.lean

Modified Mathlib/Algebra/Equiv/TransferInstance.lean

Modified Mathlib/Algebra/Lie/Semisimple/Basic.lean

modified theorem LieAlgebra.IsSimple.eq_top_of_isAtom

deleted theorem LieAlgebra.IsSimple.isAtom_iff_eq_top

deleted theorem LieAlgebra.IsSimple.isAtom_top

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

modified def LinearEquiv.arrowCongrAddEquiv

modified def LinearEquiv.conjRingEquiv

added def LinearEquiv.domMulActCongrRight

Modified Mathlib/Algebra/Module/LinearMap/Defs.lean

added theorem LinearMap.ne_zero_of_injective

added theorem LinearMap.ne_zero_of_surjective

Modified Mathlib/Algebra/Module/LinearMap/End.lean

modified theorem Module.End.intCast_def

modified theorem Module.End.natCast_def

deleted def Module.moduleEndSelf

deleted def Module.moduleEndSelfOp

modified def Module.toModuleEnd

added def RingEquiv.moduleEndSelf

added def RingEquiv.moduleEndSelfOp

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

added theorem LinearMap.exists_ne_zero_of_sSup_eq_top

added theorem LinearMap.le_ker_iff_comp_subtype_eq_zero

Modified Mathlib/Data/Matrix/Basic.lean

added def AlgEquiv.mopMatrix

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem IsAlgClosed.algebraMap_bijective_of_isIntegral

deleted theorem IsAlgClosed.algebraMap_surjective_of_isIntegral

added theorem IsAlgClosed.ringHom_bijective_of_isIntegral

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

modified def LinearEquiv.algConj

Modified Mathlib/LinearAlgebra/Projection.lean

added theorem Submodule.linearProjOfIsCompl_surjective

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem LinearMap.exists_ne_zero_of_sSup_eq

Modified Mathlib/Logic/Equiv/Defs.lean

added theorem Equiv.nontrivial_congr

Modified Mathlib/Order/Atoms.lean

added theorem isAtom_iff_eq_top

added theorem isCoatom_iff_eq_bot

modified theorem «Prop».isAtom_iff

modified theorem «Prop».isCoatom_iff

Modified Mathlib/RingTheory/Congruence/Basic.lean

added theorem RingCon.nontrivial_iff

added theorem RingCon.subsingleton_iff

Modified Mathlib/RingTheory/Ideal/Defs.lean

Modified Mathlib/RingTheory/Jacobson/Ideal.lean

deleted theorem Ideal.jacobson_mul_mem_right

Modified Mathlib/RingTheory/LocalRing/RingHom/Basic.lean

Modified Mathlib/RingTheory/Nullstellensatz.lean

Modified Mathlib/RingTheory/SimpleRing/Congr.lean

added theorem isSimpleRing_iff_isTwoSided_imp

Modified Mathlib/RingTheory/SimpleRing/Defs.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

modified theorem Ideal.asIdeal_toTwoSided

modified theorem Ideal.coe_toTwoSided

modified theorem Ideal.mem_toTwoSided

modified def Ideal.toTwoSided

modified theorem Ideal.toTwoSided_asIdeal

added theorem TwoSidedIdeal.bot_asIdeal

added def TwoSidedIdeal.orderIsoIsTwoSided

added theorem TwoSidedIdeal.top_asIdeal

Modified Mathlib/RingTheory/Unramified/Field.lean