Documentation Verification Report

AlgebraicClosure

📁 Source: Mathlib/FieldTheory/AlgebraicClosure.lean

Statistics

Metric	Count
Definitions `algebraicClosure`, `algebraicClosure`, `algEquivOfAlgEquiv`	3
Theorems `isAlgebraic_adjoin_iff_isAlgebraic`, `algebraicClosure_eq_bot_iff`, `algebraicClosure`, `algebraicClosure`, `adjoin_le`, `algebraicClosure_eq_bot`, `comap_eq_of_algHom`, `eq_restrictScalars_of_isAlgebraic`, `eq_top_iff`, `isAlgClosure`, `isAlgebraic`, `isIntegralClosure`, `le_restrictScalars`, `map_eq_of_algEquiv`, `map_eq_of_algebraicClosure_eq_bot`, `map_le_of_algHom`, `normalClosure_eq_self`, `algebraicClosure_toSubalgebra`, `le_algebraicClosure`, `le_algebraicClosure'`, `le_algebraicClosure_iff`, `map_mem_algebraicClosure_iff`, `mem_algebraicClosure_iff`, `mem_algebraicClosure_iff'`	24
Total	27

AlgEquiv

Definitions

Name	Category	Theorems
`algebraicClosure` 📖	CompOp	—

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAlgebraic_adjoin_iff_isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `toField` `algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `IsAlgebraic`	—	`IsScalarTower.left` `le_algebraicClosure_iff` `adjoin_le_iff` `Iff.imp` `mem_algebraicClosure_iff`

IsAlgClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicClosure_eq_bot_iff` 📖	mathematical	—	`algebraicClosure` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `IsAlgClosed`	—	`of_exists_root` `exists_aeval_eq_zero` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LT.lt.ne'` `Polynomial.degree_pos_of_irreducible` `mem_algebraicClosure_iff'` `minpoly.ne_zero_iff` `ne_zero_of_dvd_ne_zero` `Polynomial.Monic.ne_zero` `minpoly.dvd` `IsScalarTower.left` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic` `algebraicClosure.isAlgebraic`

Splits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicClosure` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap`	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `IntermediateField.toField` `IntermediateField.algebra'` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IntermediateField.splits_of_splits` `instIsDomain` `IsAlgebraic.isIntegral` `isAlgebraic_of_mem_rootSet`

Transcendental

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicClosure` 📖	mathematical	`Transcendental` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield`	—	`extendScalars` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `algebraicClosure.isAlgebraic`

(root)

Definitions

Name	Category	Theorems
`algebraicClosure` 📖	CompOp	23 math math: `algebraicClosure.algebraicClosure_eq_bot`, `algebraicClosure.normalClosure_eq_self`, `algebraicClosure.isAlgebraic`, `algebraicClosure.isIntegralClosure`, `mem_algebraicClosure_iff`, `le_algebraicClosure`, `Splits.algebraicClosure`, `Transcendental.algebraicClosure`, `algebraicClosure.map_le_of_algHom`, `algebraicClosure.le_restrictScalars`, `algebraicClosure_toSubalgebra`, `algebraicClosure.eq_top_iff`, `algebraicClosure.adjoin_le`, `map_mem_algebraicClosure_iff`, `mem_algebraicClosure_iff'`, `le_algebraicClosure_iff`, `AlgebraicIndependent.algebraicClosure`, `algebraicClosure.isAlgClosure`, `IsAlgClosed.algebraicClosure_eq_bot_iff`, `algebraicClosure.map_eq_of_algEquiv`, `algebraicClosure.eq_restrictScalars_of_isAlgebraic`, `algebraicClosure.comap_eq_of_algHom`, `le_algebraicClosure'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraicClosure_toSubalgebra` 📖	mathematical	—	`IntermediateField.toSubalgebra` `algebraicClosure` `integralClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	—
`le_algebraicClosure` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `algebraicClosure`	—	`IsScalarTower.left` `le_algebraicClosure'` `Algebra.IsAlgebraic.isAlgebraic`
`le_algebraicClosure'` 📖	mathematical	`IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	`Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `algebraicClosure`	—	`IsScalarTower.left` `Polynomial.aeval_algebraMap_eq_zero_iff` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsScalarTower.right` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.isScalarTower_mid'`
`le_algebraicClosure_iff` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `algebraicClosure` `Algebra.IsAlgebraic` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Polynomial.aeval_algebraMap_eq_zero_iff` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.isScalarTower_mid'` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsScalarTower.right` `RingHomCompTriple.comp_apply` `RingHomCompTriple.ids` `le_algebraicClosure`
`map_mem_algebraicClosure_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.funLike`	—	`IsLocalRing.toNontrivial` `Field.instIsLocalRing` `minpoly.algHom_eq` `RingHom.injective` `DivisionRing.isSimpleRing`
`mem_algebraicClosure_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`isAlgebraic_iff_isIntegral`
`mem_algebraicClosure_iff'` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	—

algebraicClosure

Definitions

Name	Category	Theorems
`algEquivOfAlgEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_le` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IntermediateField.adjoin` `SetLike.coe` `IntermediateField.instSetLike` `algebraicClosure`	—	`IntermediateField.adjoin_le_iff` `le_restrictScalars`
`algebraicClosure_eq_bot` 📖	mathematical	—	`algebraicClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`bot_unique` `IntermediateField.mem_bot` `isIntegral_trans` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Algebra.IsAlgebraic.isIntegral` `isAlgebraic` `mem_algebraicClosure_iff'`
`comap_eq_of_algHom` 📖	mathematical	—	`IntermediateField.comap` `algebraicClosure`	—	`IntermediateField.ext` `map_mem_algebraicClosure_iff`
`eq_restrictScalars_of_isAlgebraic` 📖	mathematical	—	`algebraicClosure` `IntermediateField.restrictScalars`	—	`LE.le.antisymm` `le_restrictScalars` `isIntegral_trans` `Algebra.IsAlgebraic.isIntegral`
`eq_top_iff` 📖	mathematical	—	`algebraicClosure` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Algebra.IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`mem_algebraicClosure_iff` `IntermediateField.mem_top` `top_unique` `Algebra.IsAlgebraic.isAlgebraic`
`isAlgClosure` 📖	mathematical	—	`IsAlgClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroup.toAddCommMonoid`	—	`IsScalarTower.left` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsAlgClosed.algebraicClosure_eq_bot_iff` `algebraicClosure_eq_bot` `isAlgebraic`
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `IntermediateField.isAlgebraic_iff` `IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`isIntegralClosure` 📖	mathematical	—	`IsIntegralClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.instAlgebraSubtypeMem` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.id`	—	`integralClosure.isIntegralClosure`
`le_restrictScalars` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `algebraicClosure` `IntermediateField.restrictScalars`	—	`mem_algebraicClosure_iff` `IsAlgebraic.tower_top`
`map_eq_of_algEquiv` 📖	mathematical	—	`IntermediateField.map` `AlgHomClass.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `algebraicClosure`	—	`LE.le.antisymm` `map_le_of_algHom` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_mem_algebraicClosure_iff` `AlgEquiv.apply_symm_apply`
`map_eq_of_algebraicClosure_eq_bot` 📖	mathematical	`algebraicClosure` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`IntermediateField.map` `IsScalarTower.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`le_antisymm` `map_le_of_algHom` `IntermediateField.mem_bot` `mem_algebraicClosure_iff'` `IsIntegral.tower_top` `map_mem_algebraicClosure_iff`
`map_le_of_algHom` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IntermediateField.map` `algebraicClosure`	—	`IntermediateField.map_le_iff_le_comap` `Eq.ge` `comap_eq_of_algHom`
`normalClosure_eq_self` 📖	mathematical	—	`IntermediateField.normalClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `algebraicClosure` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`le_antisymm` `IsScalarTower.left` `normalClosure_le_iff` `le_algebraicClosure` `AlgEquiv.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isAlgebraic` `IntermediateField.le_normalClosure`

---

← Back to Index