AlgebraicallyClosed

📁 Source: Mathlib/RingTheory/RootsOfUnity/AlgebraicallyClosed.lean

Statistics

Metric	Count
Definitions	0
Theorems hasEnoughRootsOfUnity, hasEnoughRootsOfUnity_pow, hasEnoughRootsOfUnity, hasEnoughRootsOfUnity_pow, hasEnoughRootsOfUnity, hasEnoughRootsOfUnity_pow	6
Total	6

AlgebraicClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasEnoughRootsOfUnity 📖	mathematical	—	HasEnoughRootsOfUnity AlgebraicClosure CommRing.toCommMonoid instCommRing	—	NeZero.of_injective MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing IsSepClosed.hasEnoughRootsOfUnity IsSepClosed.of_isAlgClosed isAlgClosed
hasEnoughRootsOfUnity_pow 📖	mathematical	—	HasEnoughRootsOfUnity AlgebraicClosure CommRing.toCommMonoid instCommRing Monoid.toNatPow Nat.instMonoid	—	NeZero.of_injective MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing IsSepClosed.hasEnoughRootsOfUnity_pow IsSepClosed.of_isAlgClosed isAlgClosed

IsSepClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasEnoughRootsOfUnity 📖	mathematical	—	HasEnoughRootsOfUnity CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain	—	NeZero.of_neZero_natCast isCyclotomicExtension Set.mem_singleton_iff IsCyclotomicExtension.exists_isPrimitiveRoot rootsOfUnity.isCyclic instIsDomain
hasEnoughRootsOfUnity_pow 📖	mathematical	—	HasEnoughRootsOfUnity CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Monoid.toNatPow Nat.instMonoid	—	NeZero.pow isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain hasEnoughRootsOfUnity

SeparableClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasEnoughRootsOfUnity 📖	mathematical	—	HasEnoughRootsOfUnity SeparableClosure CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.toField AlgebraicClosure AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield Algebra.id separableClosure	—	AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass NeZero.of_injective MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgebraicClosure.instIsScalarTower IsScalarTower.right RingHom.injective DivisionRing.isSimpleRing SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing IsSepClosed.hasEnoughRootsOfUnity isSepClosed
hasEnoughRootsOfUnity_pow 📖	mathematical	—	HasEnoughRootsOfUnity SeparableClosure CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.toField AlgebraicClosure AlgebraicClosure.instField AlgebraicClosure.instAlgebra Semifield.toCommSemiring Field.toSemifield Algebra.id separableClosure Monoid.toNatPow Nat.instMonoid	—	AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass NeZero.of_injective MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgebraicClosure.instIsScalarTower IsScalarTower.right RingHom.injective DivisionRing.isSimpleRing SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing IsSepClosed.hasEnoughRootsOfUnity_pow isSepClosed

---

← Back to Index