Documentation Verification Report

Closure

📁 Source: Mathlib/FieldTheory/Normal/Closure.lean

Statistics

Metric	Count
Definitions `algHomEmbeddingOfSplits`, `closureOperator`, `normalClosure`, `normalClosureOperator`, `IsNormalClosure`, `equiv`, `algHomEquiv`, `algebra`	8
Theorems `fieldRange_le_normalClosure`, `isNormalClosure_iff`, `isNormalClosure_normalClosure`, `normalClosure_eq_iSup_adjoin_of_splits`, `normalClosure_le_iSup_adjoin`, `le_normalClosure`, `normalClosureOperator_apply`, `normalClosureOperator_isClosed`, `normalClosure_def'`, `normalClosure_def''`, `normalClosure_le_iff_of_normal`, `normalClosure_map_eq`, `normalClosure_mono`, `normalClosure_of_normal`, `normal_iff_forall_fieldRange_eq`, `normal_iff_forall_fieldRange_le`, `normal_iff_forall_map_eq`, `normal_iff_forall_map_eq'`, `normal_iff_forall_map_le`, `normal_iff_forall_map_le'`, `normal_iff_normalClosure_eq`, `normal_iff_normalClosure_le`, `adjoin_rootSet`, `normal`, `splits`, `isNormalClosure_normalClosure`, `instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure`, `instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1`, `is_finiteDimensional`, `normal`, `restrictScalars_eq`, `normalClosure_def`, `normalClosure_eq_iSup_adjoin`, `normalClosure_eq_iSup_adjoin'`, `normalClosure_le_iff`	35
Total	43

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fieldRange_le_normalClosure` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `fieldRange` `IntermediateField.normalClosure`	—	`le_iSup`

Algebra.IsAlgebraic

Definitions

Name	Category	Theorems
`algHomEmbeddingOfSplits` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNormalClosure_iff` 📖	mathematical	—	`IsNormalClosure` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.normalClosure` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`instIsDomain` `normalClosure_eq_iSup_adjoin_of_splits`
`isNormalClosure_normalClosure` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`IsNormalClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.normalClosure` `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` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `isNormalClosure_iff` `instIsDomain` `normalClosure_eq_iSup_adjoin_of_splits` `IntermediateField.splits_of_splits` `HasSubset.Subset.trans` `Set.instIsTransSubset` `IntermediateField.subset_adjoin` `SetLike.coe_subset_coe` `instIsConcreteLE` `le_iSup` `Function.Injective.mem_set_image` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.toRingHom_eq_coe` `RingHom.coe_coe` `IntermediateField.coe_val` `IntermediateField.coe_map` `IntermediateField.map_iSup` `iSup_le` `le_iSup_of_le` `AlgHom.fieldRange_le_normalClosure` `AlgHom.map_fieldRange` `IntermediateField.val.eq_1` `AlgHom.val_comp_codRestrict` `le_refl`
`normalClosure_eq_iSup_adjoin_of_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`IntermediateField.normalClosure` `iSup` `IntermediateField` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `IntermediateField.adjoin` `Polynomial.rootSet` `instIsDomain`	—	`LE.le.antisymm` `instIsDomain` `normalClosure_le_iSup_adjoin` `iSup_le` `IntermediateField.adjoin_le_iff` `IntermediateField.exists_algHom_of_splits_of_aeval` `Algebra.IsIntegral.isIntegral` `isIntegral` `Polynomial.mem_rootSet` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `le_iSup`
`normalClosure_le_iSup_adjoin` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IntermediateField.normalClosure` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `IntermediateField.adjoin` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `Field.toSemifield`	—	`iSup_le` `instIsDomain` `le_iSup` `IntermediateField.subset_adjoin` `Polynomial.mem_rootSet_of_ne` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsIntegral.isIntegral` `isIntegral` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.toRingHom_eq_coe` `AlgHom.coe_toRingHom` `Polynomial.aeval_algHom_apply` `minpoly.aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass`

IntermediateField

Definitions

Name	Category	Theorems
`closureOperator` 📖	CompOp	—
`normalClosure` 📖	CompOp	42 math math: `normalClosure_le_iff`, `algebraicClosure.normalClosure_eq_self`, `IsGalois.normalClosure`, `normalClosure_eq_iSup_adjoin'`, `Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `normal_iff_normalClosure_le`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1`, `normalClosure.restrictScalars_eq`, `isNormalClosure_normalClosure`, `Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1`, `normalClosure_def`, `instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure`, `normalClosureOperator_apply`, `normalClosure_of_normal`, `Algebra.IsAlgebraic.isNormalClosure_iff`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `spectralNorm.eq_of_normalClosure`, `Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `spectralNorm.eq_of_normalClosure'`, `normalClosure_def''`, `FiniteGaloisIntermediateField.adjoin_val`, `Algebra.IsAlgebraic.isNormalClosure_normalClosure`, `AlgHom.fieldRange_le_normalClosure`, `Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `normalClosure_eq_iSup_adjoin`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `normalClosure.normal`, `normalClosure_mono`, `normalClosure_le_iff_of_normal`, `normalClosure_map_eq`, `Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `le_normalClosure`, `normalClosure_def'`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1`, `Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits`, `normalClosure.is_finiteDimensional`, `Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin`, `normal_iff_normalClosure_eq`, `separableClosure.normalClosure_eq_self`
`normalClosureOperator` 📖	CompOp	2 math math: `normalClosureOperator_apply`, `normalClosureOperator_isClosed`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_normalClosure` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalClosure` `SetLike.instMembership` `instSetLike` `toField` `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`	—	`Eq.trans_le` `IsScalarTower.left` `fieldRange_val` `AlgHom.fieldRange_le_normalClosure`
`normalClosureOperator_apply` 📖	mathematical	—	`DFunLike.coe` `ClosureOperator` `IntermediateField` `PartialOrder.toPreorder` `instPartialOrder` `ClosureOperator.instFunLike` `normalClosureOperator` `normalClosure` `SetLike.instMembership` `instSetLike` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id`	—	—
`normalClosureOperator_isClosed` 📖	mathematical	—	`ClosureOperator.IsClosed` `IntermediateField` `PartialOrder.toPreorder` `instPartialOrder` `normalClosureOperator`	—	—
`normalClosure_def'` 📖	mathematical	—	`normalClosure` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `iSup` `AlgHom` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `map`	—	`IsScalarTower.left` `normalClosure_def` `le_antisymm` `iSup_le` `le_iSup_of_le` `isScalarTower_mid'` `IsScalarTower.right` `AlgHom.liftNormal_commutes`
`normalClosure_def''` 📖	mathematical	—	`normalClosure` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `iSup` `AlgEquiv` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `map` `AlgHomClass.toAlgHom` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass`	—	`IsScalarTower.left` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `normalClosure_def'` `le_antisymm` `iSup_le` `le_iSup_of_le` `IsScalarTower.right` `AlgHom.restrictNormal_commutes` `le_rfl`
`normalClosure_le_iff_of_normal` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalClosure` `SetLike.instMembership` `instSetLike` `toField` `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`	—	`IsScalarTower.left` `fieldRange_val` `normalClosure_le_iff` `normalClosure_of_normal` `normalClosure_mono`
`normalClosure_map_eq` 📖	mathematical	—	`normalClosure` `IntermediateField` `SetLike.instMembership` `instSetLike` `map` `toField` `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`	—	`AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IsScalarTower.left` `normalClosure_def''` `map_map` `Equiv.iSup_congr` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Normal.toIsAlgebraic`
`normalClosure_mono` 📖	mathematical	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`normalClosure` `SetLike.instMembership` `instSetLike` `toField` `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`	—	`IsScalarTower.left` `normalClosure_def'` `iSup_mono` `map_mono`
`normalClosure_of_normal` 📖	mathematical	—	`normalClosure` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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`	—	`IsScalarTower.left` `AlgHom.fieldRange_of_normal` `iSup_const`
`normal_iff_forall_fieldRange_eq` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `AlgHom.fieldRange`	—	`IsScalarTower.left` `AlgHom.fieldRange_of_normal` `normal_iff_forall_fieldRange_le` `Eq.le`
`normal_iff_forall_fieldRange_le` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `AlgHom.fieldRange`	—	`IsScalarTower.left` `normal_iff_normalClosure_le` `normalClosure_def` `iSup_le_iff`
`normal_iff_forall_map_eq` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `map`	—	`IsScalarTower.left` `AlgHom.map_fieldRange` `fieldRange_val` `normal_iff_forall_fieldRange_eq` `normal_iff_forall_map_le` `Eq.le`
`normal_iff_forall_map_eq'` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `map` `AlgHomClass.toAlgHom` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass`	—	`IsScalarTower.left` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `normal_iff_forall_map_eq` `normal_iff_forall_map_le'` `Eq.le`
`normal_iff_forall_map_le` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map`	—	`IsScalarTower.left` `normal_iff_normalClosure_le` `normalClosure_def'` `iSup_le_iff`
`normal_iff_forall_map_le'` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `AlgHomClass.toAlgHom` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass`	—	`IsScalarTower.left` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `normal_iff_normalClosure_le` `normalClosure_def''` `iSup_le_iff`
`normal_iff_normalClosure_eq` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `normalClosure`	—	`IsScalarTower.left` `normalClosure_of_normal` `normalClosure.normal`
`normal_iff_normalClosure_le` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `normalClosure`	—	`IsScalarTower.left` `normal_iff_normalClosure_eq` `LE.le.ge_iff_eq'` `le_normalClosure`

IsNormalClosure

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_rootSet` 📖	mathematical	—	`iSup` `IntermediateField` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `IntermediateField.adjoin` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `Field.toSemifield` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—
`normal` 📖	mathematical	—	`Normal`	—	`Normal.of_algEquiv` `IsScalarTower.left` `instIsDomain` `IntermediateField.normal_iSup` `Normal.of_isSplittingField` `IntermediateField.adjoin_rootSet_isSplittingField` `splits` `adjoin_rootSet`
`splits` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	—

(root)

Definitions

Name	Category	Theorems
`IsNormalClosure` 📖	CompData	3 math math: `isNormalClosure_normalClosure`, `Algebra.IsAlgebraic.isNormalClosure_iff`, `Algebra.IsAlgebraic.isNormalClosure_normalClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNormalClosure_normalClosure` 📖	mathematical	—	`IsNormalClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.normalClosure` `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`	—	`IsScalarTower.left` `Algebra.IsAlgebraic.isNormalClosure_normalClosure` `Algebra.IsAlgebraic.of_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Normal.toIsAlgebraic` `minpoly.algHom_eq` `Normal.splits`
`normalClosure_def` 📖	mathematical	—	`IntermediateField.normalClosure` `iSup` `IntermediateField` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `AlgHom.fieldRange`	—	—
`normalClosure_eq_iSup_adjoin` 📖	mathematical	—	`IntermediateField.normalClosure` `iSup` `IntermediateField` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `IntermediateField.adjoin` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `Field.toSemifield`	—	`normalClosure_eq_iSup_adjoin'`
`normalClosure_eq_iSup_adjoin'` 📖	mathematical	—	`IntermediateField.normalClosure` `iSup` `IntermediateField` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `IntermediateField.adjoin` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `minpoly` `DivisionRing.toRing` `Field.toDivisionRing` `instIsDomain` `Field.toSemifield`	—	`instIsDomain` `Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits` `Algebra.IsAlgebraic.of_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Normal.toIsAlgebraic` `minpoly.algHom_eq` `Normal.splits`
`normalClosure_le_iff` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IntermediateField.normalClosure` `AlgHom.fieldRange`	—	`iSup_le_iff`

normalClosure

Definitions

Name	Category	Theorems
`algHomEquiv` 📖	CompOp	—
`algebra` 📖	CompOp	9 math math: `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1`, `restrictScalars_eq`, `instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1`, `Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `spectralNorm.eq_of_normalClosure`, `Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `spectralNorm.eq_of_normalClosure'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure` 📖	mathematical	—	`IsScalarTower` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.normalClosure` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.toField` `algebra` `IntermediateField.algebra'` `CommSemiring.toSemiring` `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`	—	`IsScalarTower.of_algebraMap_eq'` `IsScalarTower.left` `RingHom.ext` `IsScalarTower.algebraMap_apply`
`instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1` 📖	mathematical	—	`IsScalarTower` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.normalClosure` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.toField` `algebra` `IntermediateField.instSMulSubtypeMem` `CommSemiring.toSemiring` `Algebra.id`	—	`IsScalarTower.of_algebraMap_eq'` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass`
`is_finiteDimensional` 📖	mathematical	—	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.normalClosure` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `IntermediateField.toField` `IntermediateField.module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `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`	—	`IntermediateField.finiteDimensional_iSup_of_finite` `Finite.algHom` `Module.Free.of_divisionRing` `instIsDomain` `LinearMap.finiteDimensional_range`
`normal` 📖	mathematical	—	`Normal` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.normalClosure` `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`	—	`IsScalarTower.left` `isEmpty_or_nonempty` `IntermediateField.normalClosure.eq_1` `iSup_of_empty` `Normal.of_algEquiv` `normal_self` `IsNormalClosure.normal` `isNormalClosure_normalClosure`
`restrictScalars_eq` 📖	mathematical	—	`IntermediateField.restrictScalars` `AlgHom.fieldRange` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.normalClosure` `IntermediateField.toField` `algebra` `IsScalarTower.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.instAlgebraSubtypeMem` `Algebra.id` `instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1`	—	`SetLike.ext'` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1` `Subtype.range_val`

---

← Back to Index