IsAlgClosed

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

Statistics

Metric	Count
Definitions IsAlgClosed	1
Theorems exists_algEquiv_pi_matrix_of_isAlgClosed, exists_algEquiv_matrix_of_isAlgClosed	2
Total	3

IsSemisimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_algEquiv_pi_matrix_of_isAlgClosed 📖	mathematical	—	MulZeroClass.toZero Nat.instMulZeroClass AlgEquiv Semifield.toCommSemiring Field.toSemifield Ring.toSemiring Pi.semiring Matrix Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Fin.fintype Pi.algebra Matrix.instAlgebra Algebra.id	—	exists_algEquiv_pi_matrix_divisionRing_finite IsAlgClosed.algebraMap_bijective_of_isIntegral DivisionRing.isDomain Algebra.IsAlgebraic.isIntegral Algebra.IsAlgebraic.of_finite IsLocalRing.toNontrivial Field.instIsLocalRing

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_algEquiv_matrix_of_isAlgClosed 📖	mathematical	—	AlgEquiv Matrix Semifield.toCommSemiring Field.toSemifield Ring.toSemiring Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Fin.fintype Matrix.instAlgebra Algebra.id	—	IsArtinianRing.of_finite IsScalarTower.right instIsArtinianOfIsSemisimpleModuleOfFinite IsSemisimpleRing.isSemisimpleModule instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self exists_algEquiv_matrix_divisionRing_finite IsAlgClosed.algebraMap_bijective_of_isIntegral DivisionRing.isDomain Algebra.IsAlgebraic.isIntegral Algebra.IsAlgebraic.of_finite IsLocalRing.toNontrivial Field.instIsLocalRing

(root)

Definitions

Name	Category	Theorems
IsAlgClosed 📖	CompData	9 math math: IsAlgClosed.of_ringEquiv, IsAlgClosure.isAlgClosed, IsSepClosed.isAlgClosed_of_perfectField, FirstOrder.Field.isAlgClosed_of_model_ACF, isAlgClosure_iff, IsAlgClosed.of_exists_root, AlgebraicClosure.isAlgClosed, IsAlgClosed.algebraicClosure_eq_bot_iff, Complex.isAlgClosed

---

← Back to Index