Documentation Verification Report

WedderburnArtin

📁 Source: Mathlib/RingTheory/SimpleModule/WedderburnArtin.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_end_algEquiv`, `exists_end_algEquiv_pi_matrix_divisionRing`, `exists_end_algEquiv_pi_matrix_end`, `exists_end_ringEquiv`, `exists_end_ringEquiv_pi_matrix_divisionRing`, `exists_end_ringEquiv_pi_matrix_end`, `exists_algEquiv_pi_matrix_divisionRing`, `exists_algEquiv_pi_matrix_divisionRing_finite`, `exists_algEquiv_pi_matrix_end_mulOpposite`, `exists_ringEquiv_pi_matrix_divisionRing`, `exists_ringEquiv_pi_matrix_end_mulOpposite`, `instMatrix`, `instMulOpposite`, `moduleEnd`, `exists_algEquiv_matrix_divisionRing`, `exists_algEquiv_matrix_divisionRing_finite`, `exists_algEquiv_matrix_end_mulOpposite`, `exists_ringEquiv_matrix_divisionRing`, `exists_ringEquiv_matrix_end_mulOpposite`, `instIsSemisimpleRing`, `isIsotypic`, `isSemisimpleRing_iff_isArtinianRing`, `isSemisimpleRing_iff_pi_matrix_divisionRing`, `isSemisimpleRing_mulOpposite_iff`, `isSimpleRing_isArtinianRing_iff`	25
Total	25

IsSemisimpleModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_end_algEquiv` 📖	mathematical	—	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AlgEquiv` `Module.End` `Module.End.instSemiring` `Pi.semiring` `Matrix` `Submodule.addCommMonoid` `Matrix.semiring` `Fin.fintype` `Module.End.instAlgebra` `IsScalarTower.to_smulCommClass'` `Algebra.toSMul` `Pi.algebra` `Matrix.instAlgebra` `Submodule.module'` `CommSemiring.toSemiring` `Submodule.isScalarTower'` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid`	—	`exists_end_algEquiv_pi_matrix_end`
`exists_end_algEquiv_pi_matrix_divisionRing` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `AlgEquiv` `Module.End` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instSemiring` `Pi.semiring` `Matrix` `Matrix.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Fin.fintype` `Module.End.instAlgebra` `IsScalarTower.to_smulCommClass'` `Algebra.toSMul` `Pi.algebra` `Matrix.instAlgebra`	—	`IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `IsScalarTower.left` `exists_end_algEquiv_pi_matrix_end`
`exists_end_algEquiv_pi_matrix_end` 📖	mathematical	—	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AlgEquiv` `Module.End` `Module.End.instSemiring` `Pi.semiring` `Matrix` `Submodule.addCommMonoid` `Matrix.semiring` `Fin.fintype` `Module.End.instAlgebra` `IsScalarTower.to_smulCommClass'` `Algebra.toSMul` `Pi.algebra` `Matrix.instAlgebra` `Submodule.module'` `CommSemiring.toSemiring` `Submodule.isScalarTower'` `SMulZeroClass.toSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsScalarTower.left` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid`	—	`RingHomInvPair.ids` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `IsScalarTower.left` `instFiniteElemSubmoduleIsotypicComponentsOfIsNoetherian` `instIsNoetherianOfFinite` `Function.smulCommClass` `Pi.isScalarTower` `IsIsotypic.submodule_linearEquiv_fun` `Module.IsNoetherian.finite` `isNoetherian_submodule'` `instNontrivialSubtypeMemSubmoduleValSetIsotypicComponents` `IsIsotypic.isotypicComponents`
`exists_end_ringEquiv` 📖	mathematical	—	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `MulZeroClass.toZero` `Nat.instMulZeroClass` `RingEquiv` `Module.End` `Module.End.instMul` `Pi.instMul` `Matrix` `Submodule.addCommMonoid` `Matrix.instMulOfFintypeOfAddCommMonoid` `Fin.fintype` `LinearMap.addCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instAdd` `Pi.instAdd` `Matrix.add`	—	`exists_end_ringEquiv_pi_matrix_end`
`exists_end_ringEquiv_pi_matrix_divisionRing` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `RingEquiv` `Module.End` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instMul` `Pi.instMul` `Matrix` `Matrix.instMulOfFintypeOfAddCommMonoid` `Fin.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `DivisionRing.toRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `LinearMap.instAdd` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.instAdd` `Matrix.add` `Distrib.toAdd`	—	`IsScalarTower.to_smulCommClass'` `AddCommMonoid.nat_isScalarTower` `exists_end_algEquiv_pi_matrix_divisionRing` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass`
`exists_end_ringEquiv_pi_matrix_end` 📖	mathematical	—	`IsSimpleModule` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommGroup` `Submodule.module` `MulZeroClass.toZero` `Nat.instMulZeroClass` `RingEquiv` `Module.End` `Module.End.instMul` `Pi.instMul` `Matrix` `Submodule.addCommMonoid` `Matrix.instMulOfFintypeOfAddCommMonoid` `Fin.fintype` `LinearMap.addCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instAdd` `Pi.instAdd` `Matrix.add`	—	`IsScalarTower.to_smulCommClass'` `AddCommMonoid.nat_isScalarTower` `Submodule.isScalarTower'` `IsScalarTower.left` `exists_end_algEquiv_pi_matrix_end` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass`

IsSemisimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_algEquiv_pi_matrix_divisionRing` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `AlgEquiv` `Ring.toSemiring` `Pi.semiring` `Matrix` `Matrix.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Fin.fintype` `Pi.algebra` `Matrix.instAlgebra`	—	`IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `IsScalarTower.left` `exists_algEquiv_pi_matrix_end_mulOpposite`
`exists_algEquiv_pi_matrix_divisionRing_finite` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `AlgEquiv` `Ring.toSemiring` `Pi.semiring` `Matrix` `Matrix.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Fin.fintype` `Pi.algebra` `Matrix.instAlgebra`	—	`exists_algEquiv_pi_matrix_divisionRing` `Module.Finite.equiv` `RingHomCompTriple.ids` `Module.Finite.of_surjective` `RingHomSurjective.ids` `Function.update_self`
`exists_algEquiv_pi_matrix_end_mulOpposite` 📖	mathematical	—	`IsSimpleModule` `Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.addCommGroup` `Ring.toAddCommGroup` `Submodule.module` `MulZeroClass.toZero` `Nat.instMulZeroClass` `AlgEquiv` `Pi.semiring` `Matrix` `MulOpposite` `Module.End` `Submodule.addCommMonoid` `Matrix.semiring` `MulOpposite.instSemiring` `Module.End.instSemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Fin.fintype` `Pi.algebra` `Matrix.instAlgebra` `MulOpposite.instAlgebra` `Module.End.instAlgebra` `Submodule.module'` `CommSemiring.toSemiring` `Algebra.toSMul` `Algebra.toModule` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocSemiring.toMulZeroClass` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.to_smulCommClass'` `IsScalarTower.right` `Submodule.isScalarTower'` `IsScalarTower.left` `IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end` `Module.Finite.self`
`exists_ringEquiv_pi_matrix_divisionRing` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Pi.instMul` `Matrix` `Matrix.instMulOfFintypeOfAddCommMonoid` `Fin.fintype` `DivisionRing.toRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toAdd` `Pi.instAdd` `Matrix.add`	—	`exists_algEquiv_pi_matrix_divisionRing` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass`
`exists_ringEquiv_pi_matrix_end_mulOpposite` 📖	mathematical	—	`IsSimpleModule` `Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.addCommGroup` `Ring.toAddCommGroup` `Submodule.module` `MulZeroClass.toZero` `Nat.instMulZeroClass` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Pi.instMul` `Matrix` `MulOpposite` `Module.End` `Submodule.addCommMonoid` `Matrix.instMulOfFintypeOfAddCommMonoid` `Fin.fintype` `MulOpposite.instMul` `Module.End.instMul` `MulOpposite.instAddCommMonoid` `LinearMap.addCommMonoid` `RingHom.id` `Distrib.toAdd` `Pi.instAdd` `Matrix.add` `MulOpposite.instAdd` `LinearMap.instAdd`	—	`IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `IsScalarTower.left` `exists_algEquiv_pi_matrix_end_mulOpposite` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass`
`instMatrix` 📖	mathematical	—	`IsSemisimpleRing` `Matrix` `Matrix.instRing`	—	`isEmpty_or_nonempty` `isSemisimpleModule` `instIsSemisimpleRingOfSubsingleton` `Matrix.subsingleton_of_empty_right` `exists_ringEquiv_pi_matrix_divisionRing` `RingEquiv.isSemisimpleRing` `instIsSemisimpleRingForallOfFinite` `Finite.of_fintype` `IsSimpleRing.instIsSemisimpleRing` `IsSimpleRing.matrix` `DivisionRing.isSimpleRing` `instIsArtinianRingMatrix` `instIsArtinianOfIsSemisimpleModuleOfFinite` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.Finite.self`
`instMulOpposite` 📖	mathematical	—	`IsSemisimpleRing` `MulOpposite` `MulOpposite.instRing`	—	`exists_ringEquiv_pi_matrix_divisionRing` `RingEquiv.isSemisimpleRing` `instIsSemisimpleRingForallOfFinite` `Finite.of_fintype` `instMatrix` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule`
`moduleEnd` 📖	mathematical	—	`IsSemisimpleRing` `Module.End` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instRing`	—	`IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing` `RingEquiv.isSemisimpleRing` `instIsSemisimpleRingForallOfFinite` `Finite.of_fintype` `isSemisimpleModule` `IsSimpleRing.instIsSemisimpleRing` `IsSimpleRing.matrix` `DivisionRing.isSimpleRing` `instIsArtinianRingMatrix` `instIsArtinianOfIsSemisimpleModuleOfFinite` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule` `Module.Finite.self`

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_algEquiv_matrix_divisionRing` 📖	mathematical	—	`AlgEquiv` `Matrix` `Ring.toSemiring` `Matrix.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Fin.fintype` `Matrix.instAlgebra`	—	`IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `IsScalarTower.left` `exists_algEquiv_matrix_end_mulOpposite`
`exists_algEquiv_matrix_divisionRing_finite` 📖	mathematical	—	`AlgEquiv` `Matrix` `Ring.toSemiring` `Matrix.semiring` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Fin.fintype` `Matrix.instAlgebra`	—	`IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `IsScalarTower.left` `exists_algEquiv_matrix_end_mulOpposite` `Module.Finite.equiv` `Module.Finite.of_surjective` `RingHomSurjective.ids`
`exists_algEquiv_matrix_end_mulOpposite` 📖	mathematical	—	`AlgEquiv` `Matrix` `MulOpposite` `Module.End` `Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.addCommMonoid` `Submodule.module` `Matrix.semiring` `MulOpposite.instSemiring` `Module.End.instSemiring` `Fin.fintype` `Matrix.instAlgebra` `MulOpposite.instAlgebra` `Module.End.instAlgebra` `Submodule.module'` `CommSemiring.toSemiring` `Algebra.toSMul` `Algebra.toModule` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsScalarTower.left`	—	`RingHomInvPair.ids` `IsScalarTower.right` `IsScalarTower.to_smulCommClass'` `Submodule.isScalarTower'` `IsScalarTower.left` `IsIsotypic.linearEquiv_fun` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleRing` `Module.Finite.self` `instNontrivial` `isIsotypic` `Function.smulCommClass` `Pi.isScalarTower`
`exists_ringEquiv_matrix_divisionRing` 📖	mathematical	—	`RingEquiv` `Matrix` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Matrix.instMulOfFintypeOfAddCommMonoid` `Fin.fintype` `DivisionRing.toRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toAdd` `Matrix.add`	—	`exists_ringEquiv_matrix_end_mulOpposite`
`exists_ringEquiv_matrix_end_mulOpposite` 📖	mathematical	—	`RingEquiv` `Matrix` `MulOpposite` `Module.End` `Ideal` `Ring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.addCommMonoid` `Submodule.module` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Matrix.instMulOfFintypeOfAddCommMonoid` `Fin.fintype` `MulOpposite.instMul` `Module.End.instMul` `MulOpposite.instAddCommMonoid` `LinearMap.addCommMonoid` `RingHom.id` `Distrib.toAdd` `Matrix.add` `MulOpposite.instAdd` `LinearMap.instAdd`	—	`RingHomInvPair.ids` `IsIsotypic.linearEquiv_fun` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleRing` `Module.Finite.self` `instNontrivial` `isIsotypic`
`instIsSemisimpleRing` 📖	mathematical	—	`IsSemisimpleRing`	—	`isSimpleRing_isArtinianRing_iff`
`isIsotypic` 📖	mathematical	—	`IsIsotypic`	—	`IsIsotypic.of_self` `IsSemisimpleRing.isSemisimpleModule` `instIsSemisimpleRing` `isSimpleRing_isArtinianRing_iff`
`isSemisimpleRing_iff_isArtinianRing` 📖	mathematical	—	`IsSemisimpleRing` `IsArtinianRing` `Ring.toSemiring`	—	`List.TFAE.out` `tfae`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSemisimpleRing_iff_pi_matrix_divisionRing` 📖	mathematical	—	`IsSemisimpleRing` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Pi.instMul` `Matrix` `Matrix.instMulOfFintypeOfAddCommMonoid` `Fin.fintype` `DivisionRing.toRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toAdd` `Pi.instAdd` `Matrix.add`	—	`IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing` `RingEquiv.isSemisimpleRing` `instIsSemisimpleRingForallOfFinite` `Finite.of_fintype` `IsSemisimpleRing.instMatrix` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule`
`isSemisimpleRing_mulOpposite_iff` 📖	mathematical	—	`IsSemisimpleRing` `MulOpposite` `MulOpposite.instRing`	—	`RingEquiv.isSemisimpleRing` `IsSemisimpleRing.instMulOpposite`
`isSimpleRing_isArtinianRing_iff` 📖	mathematical	—	`IsSimpleRing` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `IsArtinianRing` `Ring.toSemiring` `IsSemisimpleRing` `IsIsotypic` `Ring.toAddCommGroup` `Semiring.toModule` `Nontrivial`	—	`IsSimpleRing.isSemisimpleRing_iff_isArtinianRing` `instIsArtinianOfIsSemisimpleModuleOfFinite` `Module.Finite.self`

---

← Back to Index