Documentation Verification Report

SeparableClosure

📁 Source: Mathlib/FieldTheory/SeparableClosure.lean

Statistics

Metric	Count
Definitions `separableClosure`, `finInsepDegree`, `insepDegree`, `sepDegree`, `SeparableClosure`, `separableClosure`, `algEquivOfAlgEquiv`, `separableClosureOperator`	8
Theorems `finInsepDegree_eq`, `insepDegree_eq`, `sepDegree_eq`, `finInsepDegree_def'`, `finInsepDegree_eq_of_equiv`, `finInsepDegree_self`, `finInsepDegree_top_le_finInsepDegree_of_isScalarTower`, `insepDegree_eq_of_equiv`, `insepDegree_le_of_left_le`, `insepDegree_le_rank`, `insepDegree_self`, `insepDegree_top_le_insepDegree_of_isScalarTower`, `instNeZeroFinInsepDegree`, `instNeZeroInsepDegree`, `instNeZeroSepDegree`, `lift_insepDegree_eq_of_equiv`, `lift_sepDegree_eq_of_equiv`, `sepDegree_eq_of_equiv`, `sepDegree_le_rank`, `sepDegree_mul_insepDegree`, `sepDegree_self`, `exists_finset_maximalFor_isTranscendenceBasis_separableClosure`, `exists_finset_maximalFor_isTranscendenceBasis_separableClosure`, `finInsepDegree_bot`, `finInsepDegree_bot'`, `finInsepDegree_le_of_left_le`, `finInsepDegree_top`, `insepDegree_bot`, `insepDegree_bot'`, `insepDegree_top`, `isSeparable_adjoin_iff_isSeparable`, `isSeparable_iSup`, `isSeparable_sup`, `lift_insepDegree_bot'`, `lift_sepDegree_bot'`, `sepDegree_bot`, `sepDegree_bot'`, `sepDegree_top`, `separableClosure_eq_bot_iff`, `isSepClosed`, `isClosed_restrictScalars_separableClosure`, `le_restrictScalars_separableClosure`, `le_separableClosure`, `le_separableClosure'`, `le_separableClosure_iff`, `map_mem_separableClosure_iff`, `mem_separableClosure_iff`, `adjoin_le`, `comap_eq_of_algHom`, `eq_restrictScalars_of_isSeparable`, `eq_top_iff`, `isAlgebraic`, `isGalois`, `isSepClosure`, `isSeparable`, `le_restrictScalars`, `map_eq_of_algEquiv`, `map_eq_of_separableClosure_eq_bot`, `map_le_of_algHom`, `normalClosure_eq_self`, `separableClosure_eq_bot`, `separableClosure_le_separableClosure_iff`	62
Total	70

AlgEquiv

Definitions

Name	Category	Theorems
`separableClosure` 📖	CompOp	—

Algebra.IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finInsepDegree_eq` 📖	mathematical	—	`Field.finInsepDegree`	—	`insepDegree_eq` `Cardinal.one_toNat`
`insepDegree_eq` 📖	mathematical	—	`Field.insepDegree` `Cardinal` `Cardinal.instOne`	—	`Field.insepDegree.eq_1` `separableClosure.eq_top_iff` `IntermediateField.rank_top`
`sepDegree_eq` 📖	mathematical	—	`Field.sepDegree` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`Field.sepDegree.eq_1` `separableClosure.eq_top_iff` `IsScalarTower.left` `IntermediateField.rank_top'`

Field

Definitions

Name	Category	Theorems
`finInsepDegree` 📖	CompOp	15 math math: `IntermediateField.finInsepDegree_top`, `IsPurelyInseparable.finInsepDegree_eq`, `finSepDegree_mul_finInsepDegree`, `finInsepDegree_self`, `IntermediateField.finInsepDegree_le_of_left_le`, `finInsepDegree_eq_pow`, `finInsepDegree_eq_of_equiv`, `IntermediateField.finInsepDegree_bot'`, `finInsepDegree_mul_finInsepDegree_of_isAlgebraic`, `Algebra.IsSeparable.finInsepDegree_eq`, `IntermediateField.finInsepDegree_bot`, `finInsepDegree_def'`, `isSeparable_iff_finInsepDegree_eq_one`, `finInsepDegree_top_le_finInsepDegree_of_isScalarTower`, `instNeZeroFinInsepDegree`
`insepDegree` 📖	CompOp	20 math math: `lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`, `IntermediateField.lift_insepDegree_bot'`, `IsPurelyInseparable.insepDegree_eq`, `insepDegree_le_rank`, `insepDegree_mul_insepDegree_of_isAlgebraic`, `insepDegree_eq_of_equiv`, `instNeZeroInsepDegree`, `IntermediateField.insepDegree_bot'`, `rank_mul_insepDegree_of_isPurelyInseparable`, `lift_rank_mul_lift_insepDegree_of_isPurelyInseparable`, `sepDegree_mul_insepDegree`, `insepDegree_self`, `Algebra.IsSeparable.insepDegree_eq`, `finInsepDegree_def'`, `lift_insepDegree_eq_of_equiv`, `insepDegree_top_le_insepDegree_of_isScalarTower`, `IntermediateField.insepDegree_bot`, `IntermediateField.insepDegree_top`, `insepDegree_le_of_left_le`, `insepDegree_eq_of_isSeparable`
`sepDegree` 📖	CompOp	22 math math: `sepDegree_self`, `IsPurelyInseparable.sepDegree_eq_one`, `rank_mul_sepDegree_of_isSeparable`, `Emb.cardinal_eq`, `sepDegree_eq_of_isPurelyInseparable`, `lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, `IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable'`, `IntermediateField.sepDegree_bot`, `IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable`, `IntermediateField.lift_sepDegree_bot'`, `IntermediateField.sepDegree_bot'`, `sepDegree_mul_insepDegree`, `instNeZeroSepDegree`, `sepDegree_eq_of_isPurelyInseparable_of_isSeparable`, `Algebra.IsSeparable.sepDegree_eq`, `finSepDegree_eq`, `lift_sepDegree_eq_of_equiv`, `lift_rank_mul_lift_sepDegree_of_isSeparable`, `sepDegree_le_rank`, `sepDegree_mul_sepDegree_of_isAlgebraic`, `sepDegree_eq_of_equiv`, `IntermediateField.sepDegree_top`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finInsepDegree_def'` 📖	mathematical	—	`finInsepDegree` `DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Cardinal.commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Cardinal.toNat` `insepDegree`	—	—
`finInsepDegree_eq_of_equiv` 📖	mathematical	—	`finInsepDegree`	—	`Cardinal.toNat_lift` `lift_insepDegree_eq_of_equiv`
`finInsepDegree_self` 📖	mathematical	—	`finInsepDegree` `Algebra.id` `Semifield.toCommSemiring` `toSemifield`	—	`finInsepDegree_def'` `insepDegree_self` `Cardinal.one_toNat`
`finInsepDegree_top_le_finInsepDegree_of_isScalarTower` 📖	mathematical	—	`finInsepDegree`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `separableClosure.le_restrictScalars` `IsScalarTower.of_algebraMap_eq'` `Module.finrank_top_le_finrank_of_isScalarTower` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `IsLocalRing.toNontrivial` `instIsLocalRing` `IntermediateField.finiteDimensional_right` `IsScalarTower.right` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing`
`insepDegree_eq_of_equiv` 📖	mathematical	—	`insepDegree`	—	`Algebra.rank_eq_of_equiv_equiv` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass`
`insepDegree_le_of_left_le` 📖	mathematical	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder`	`Cardinal` `Cardinal.instLE` `insepDegree` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `Algebra.id` `Semifield.toCommSemiring`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `IsScalarTower.of_algebraMap_eq'` `insepDegree_top_le_insepDegree_of_isScalarTower`
`insepDegree_le_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `insepDegree` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`Module.rank_top_le_rank_of_isScalarTower` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `instIsLocalRing` `IsScalarTower.right`
`insepDegree_self` 📖	mathematical	—	`insepDegree` `Algebra.id` `Semifield.toCommSemiring` `toSemifield` `Cardinal` `Cardinal.instOne`	—	`insepDegree.eq_1` `Unique.instSubsingleton` `IntermediateField.rank_top`
`insepDegree_top_le_insepDegree_of_isScalarTower` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `insepDegree`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `separableClosure.le_restrictScalars` `IsScalarTower.of_algebraMap_eq'` `Module.rank_top_le_rank_of_isScalarTower` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `SubsemiringClass.nontrivial` `IsLocalRing.toNontrivial` `instIsLocalRing` `IsScalarTower.right`
`instNeZeroFinInsepDegree` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `finInsepDegree`	—	`LT.lt.ne'` `Module.finrank_pos` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `instIsLocalRing` `IntermediateField.finiteDimensional_right` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`instNeZeroInsepDegree` 📖	mathematical	—	`Cardinal` `Cardinal.instZero` `insepDegree`	—	`LT.lt.ne'` `rank_pos` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsLocalRing.toNontrivial` `instIsLocalRing`
`instNeZeroSepDegree` 📖	mathematical	—	`Cardinal` `Cardinal.instZero` `sepDegree`	—	`LT.lt.ne'` `rank_pos` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `instIsLocalRing`
`lift_insepDegree_eq_of_equiv` 📖	mathematical	—	`Cardinal.lift` `insepDegree`	—	`Algebra.lift_rank_eq_of_equiv_equiv` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass`
`lift_sepDegree_eq_of_equiv` 📖	mathematical	—	`Cardinal.lift` `sepDegree`	—	`LinearEquiv.lift_rank_eq` `IsScalarTower.left`
`sepDegree_eq_of_equiv` 📖	mathematical	—	`sepDegree`	—	`LinearEquiv.rank_eq` `IsScalarTower.left`
`sepDegree_le_rank` 📖	mathematical	—	`Cardinal` `Cardinal.instLE` `sepDegree` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`Module.rank_bot_le_rank_of_isScalarTower` `IsScalarTower.right` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.instFaithfulSMulSubtypeMem` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `IsLocalRing.toNontrivial` `instIsLocalRing` `IntermediateField.isScalarTower_mid'`
`sepDegree_mul_insepDegree` 📖	mathematical	—	`Cardinal` `Cardinal.instMul` `sepDegree` `insepDegree` `Module.rank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`rank_mul_rank` `IsScalarTower.left` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `instIsLocalRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Module.Free.of_divisionRing` `IntermediateField.isScalarTower_mid'`
`sepDegree_self` 📖	mathematical	—	`sepDegree` `Algebra.id` `Semifield.toCommSemiring` `toSemifield` `Cardinal` `Cardinal.instOne`	—	`sepDegree.eq_1` `Unique.instSubsingleton` `IsScalarTower.left` `IntermediateField.rank_bot`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finset_maximalFor_isTranscendenceBasis_separableClosure` 📖	mathematical	—	`MaximalFor` `Set` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IsTranscendenceBasis` `Set.instMembership` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `restrictScalars` `SetLike.instMembership` `instSetLike` `adjoin` `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` `Module.toDistribMulAction` `Algebra.toModule` `instAlgebraSubtypeMem` `isScalarTower_mid'` `separableClosure` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`fg_top` `isAlgebraic_adjoin_iff_top` `Algebra.isAlgebraic_iff_isIntegral` `Algebra.isIntegral_of_surjective` `AlgEquiv.surjective` `IsScalarTower.left` `exists_isTranscendenceBasis_subset` `IsDomain.to_noZeroDivisors` `instIsDomain` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `Set.Finite.subset` `Finset.finite_toSet` `instWellFoundedLTNat` `Function.argminOn_mem` `isScalarTower_mid'` `not_lt_iff_le_imp_ge` `IsTranscendenceBasis.cardinalMk_eq` `Cardinal.mk_fintype` `Fintype.card_coe` `Algebra.finite_of_essFiniteType_of_isAlgebraic` `Algebra.EssFiniteType.of_comp` `Subtype.range_coe_subtype` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsTranscendenceBasis.isAlgebraic_field` `finiteDimensional_right` `Function.not_lt_argminOn` `finrank_lt_of_gt`
`finInsepDegree_bot` 📖	mathematical	—	`Field.finInsepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `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` `Field.finInsepDegree_eq_of_equiv` `Field.finInsepDegree_self`
`finInsepDegree_bot'` 📖	mathematical	—	`Field.finInsepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Cardinal.toNat_lift` `lift_insepDegree_bot'`
`finInsepDegree_le_of_left_le` 📖	mathematical	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Field.finInsepDegree` `SetLike.instMembership` `instSetLike` `toField` `instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring`	—	`SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsScalarTower.left` `IsScalarTower.of_algebraMap_eq'` `Field.finInsepDegree_top_le_finInsepDegree_of_isScalarTower`
`finInsepDegree_top` 📖	mathematical	—	`Field.finInsepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.finInsepDegree_def'` `insepDegree_top`
`insepDegree_bot` 📖	mathematical	—	`Field.insepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `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` `Cardinal` `Cardinal.instOne`	—	`IsScalarTower.left` `Field.lift_insepDegree_eq_of_equiv` `Cardinal.lift_one` `Field.insepDegree_self`
`insepDegree_bot'` 📖	mathematical	—	`Field.insepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.insepDegree_eq_of_equiv` `IsScalarTower.left` `isScalarTower` `IsScalarTower.right`
`insepDegree_top` 📖	mathematical	—	`Field.insepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.insepDegree_eq_of_equiv` `IsScalarTower.left` `isScalarTower`
`isSeparable_adjoin_iff_isSeparable` 📖	mathematical	—	`Algebra.IsSeparable` `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` `IsSeparable`	—	`IsScalarTower.left` `le_separableClosure_iff` `adjoin_le_iff`
`isSeparable_iSup` 📖	mathematical	`Algebra.IsSeparable` `IntermediateField` `SetLike.instMembership` `instSetLike` `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`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`IsScalarTower.left` `iSup_le`
`isSeparable_sup` 📖	mathematical	—	`Algebra.IsSeparable` `IntermediateField` `SetLike.instMembership` `instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `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`	—	`IsScalarTower.left` `le_separableClosure_iff` `sup_le`
`lift_insepDegree_bot'` 📖	mathematical	—	`Cardinal.lift` `Field.insepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.lift_insepDegree_eq_of_equiv` `IsScalarTower.left` `isScalarTower` `IsScalarTower.right`
`lift_sepDegree_bot'` 📖	mathematical	—	`Cardinal.lift` `Field.sepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.lift_sepDegree_eq_of_equiv` `IsScalarTower.left` `isScalarTower` `IsScalarTower.right`
`sepDegree_bot` 📖	mathematical	—	`Field.sepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `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` `Cardinal` `Cardinal.instOne`	—	`IsScalarTower.left` `Field.lift_sepDegree_eq_of_equiv` `Cardinal.lift_one` `Field.sepDegree_self`
`sepDegree_bot'` 📖	mathematical	—	`Field.sepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.sepDegree_eq_of_equiv` `IsScalarTower.left` `isScalarTower` `IsScalarTower.right`
`sepDegree_top` 📖	mathematical	—	`Field.sepDegree` `IntermediateField` `SetLike.instMembership` `instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `toField` `algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`Field.sepDegree_eq_of_equiv` `IsScalarTower.left` `isScalarTower`

IntermediateField.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finset_maximalFor_isTranscendenceBasis_separableClosure` 📖	mathematical	—	`MaximalFor` `Set` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IsTranscendenceBasis` `Set.instMembership` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.restrictScalars` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `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` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `separableClosure` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure`

IsSepClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`separableClosure_eq_bot_iff` 📖	mathematical	—	`separableClosure` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `IsSepClosed`	—	`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_separableClosure_iff` `Polynomial.Separable.of_dvd` `minpoly.dvd` `IsScalarTower.left` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IntermediateField.eq_bot_of_isSepClosed_of_isSeparable` `separableClosure.isSeparable`

SeparableClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSepClosed` 📖	mathematical	—	`IsSepClosed` `SeparableClosure` `IntermediateField.toField` `AlgebraicClosure` `AlgebraicClosure.instField` `AlgebraicClosure.instAlgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.id` `separableClosure`	—	`IsSepClosure.sep_closed` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `separableClosure.isSepClosure` `IsSepClosed.of_isAlgClosed` `AlgebraicClosure.isAlgClosed`

(root)

Definitions

Name	Category	Theorems
`SeparableClosure` 📖	CompOp	3 math math: `SeparableClosure.isSepClosed`, `SeparableClosure.hasEnoughRootsOfUnity_pow`, `SeparableClosure.hasEnoughRootsOfUnity`
`separableClosure` 📖	CompOp	38 math math: `SeparableClosure.isSepClosed`, `IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure`, `map_mem_separableClosure_iff`, `SeparableClosure.hasEnoughRootsOfUnity_pow`, `le_separableClosure_iff`, `separableClosure_le`, `eq_separableClosure_iff`, `separableClosure.map_le_of_algHom`, `separableClosure.eq_top_iff`, `SeparableClosure.hasEnoughRootsOfUnity`, `separableClosure_inf_perfectClosure`, `le_restrictScalars_separableClosure`, `separableClosure.adjoin_eq_of_isAlgebraic`, `eq_separableClosure`, `separableClosure.isAlgebraic`, `separableClosure.isSepClosure`, `separableClosure.isSeparable`, `separableClosure.eq_restrictScalars_of_isSeparable`, `IsSepClosed.separableClosure_eq_bot_iff`, `separableClosure.comap_eq_of_algHom`, `mem_separableClosure_iff`, `le_separableClosure'`, `separableClosure_le_iff`, `isClosed_restrictScalars_separableClosure`, `separableClosure_le_separableClosure_iff`, `separableClosure.separableClosure_eq_bot`, `le_separableClosure`, `separableClosure.map_eq_of_algEquiv`, `IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure`, `separableClosure.isGalois`, `separableClosure.eq_bot_iff`, `separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable`, `separableClosure.normalClosure_eq_self`, `Field.Emb.cardinal_separableClosure`, `separableClosure.adjoin_le`, `separableClosure.le_restrictScalars`, `separableClosure.isPurelyInseparable`, `separableClosure.eq_bot_of_isPurelyInseparable`
`separableClosureOperator` 📖	CompOp	1 math math: `isClosed_restrictScalars_separableClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed_restrictScalars_separableClosure` 📖	mathematical	—	`ClosureOperator.IsClosed` `IntermediateField` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `separableClosureOperator` `IntermediateField.restrictScalars` `separableClosure`	—	`ClosureOperator.isClosed_iff_closure_le` `Eq.le` `separableClosure.separableClosure_eq_bot`
`le_restrictScalars_separableClosure` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IntermediateField.restrictScalars` `SetLike.instMembership` `IntermediateField.instSetLike` `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` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `separableClosure`	—	`isSeparable_algebraMap`
`le_separableClosure` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `separableClosure`	—	`IsScalarTower.left` `le_separableClosure'` `Algebra.IsSeparable.isSeparable`
`le_separableClosure'` 📖	mathematical	`IsSeparable` `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` `separableClosure`	—	`IsScalarTower.left` `IntermediateField.minpoly_eq`
`le_separableClosure_iff` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `separableClosure` `Algebra.IsSeparable` `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`	—	`Subalgebra.isSeparable_iff`
`map_mem_separableClosure_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `separableClosure` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.funLike`	—	`minpoly.algHom_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`mem_separableClosure_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `separableClosure` `IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	—
`separableClosure_le_separableClosure_iff` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IntermediateField.restrictScalars` `SetLike.instMembership` `IntermediateField.instSetLike` `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` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `separableClosure`	—	`ClosureOperator.IsClosed.closure_le_iff` `isClosed_restrictScalars_separableClosure`

separableClosure

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` `separableClosure`	—	`IntermediateField.adjoin_le_iff` `le_restrictScalars`
`comap_eq_of_algHom` 📖	mathematical	—	`IntermediateField.comap` `separableClosure`	—	`IntermediateField.ext` `map_mem_separableClosure_iff`
`eq_restrictScalars_of_isSeparable` 📖	mathematical	—	`separableClosure` `IntermediateField.restrictScalars`	—	`LE.le.antisymm` `le_restrictScalars` `IsSeparable.of_algebra_isSeparable_of_isSeparable`
`eq_top_iff` 📖	mathematical	—	`separableClosure` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Algebra.IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`mem_separableClosure_iff` `IntermediateField.mem_top` `top_unique` `Algebra.IsSeparable.isSeparable`
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `separableClosure` `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` `IsSeparable.isIntegral`
`isGalois` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `separableClosure` `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` `isSeparable` `normalClosure_eq_self` `normalClosure.normal`
`isSepClosure` 📖	mathematical	—	`IsSepClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `separableClosure` `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` `IsSepClosed.separableClosure_eq_bot_iff` `separableClosure_eq_bot` `isSeparable`
`isSeparable` 📖	mathematical	—	`Algebra.IsSeparable` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `separableClosure` `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.minpoly_eq`
`le_restrictScalars` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `separableClosure` `IntermediateField.restrictScalars`	—	`IsSeparable.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` `separableClosure`	—	`LE.le.antisymm` `map_le_of_algHom` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_mem_separableClosure_iff` `AlgEquiv.apply_symm_apply`
`map_eq_of_separableClosure_eq_bot` 📖	mathematical	`separableClosure` `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_separableClosure_iff` `IsSeparable.tower_top` `map_mem_separableClosure_iff`
`map_le_of_algHom` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IntermediateField.map` `separableClosure`	—	`IntermediateField.map_le_iff_le_comap` `Eq.ge` `comap_eq_of_algHom`
`normalClosure_eq_self` 📖	mathematical	—	`IntermediateField.normalClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `separableClosure` `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` `AlgEquiv.Algebra.isSeparable` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isSeparable` `le_separableClosure` `IntermediateField.le_normalClosure`
`separableClosure_eq_bot` 📖	mathematical	—	`separableClosure` `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` `IsSeparable.of_algebra_isSeparable_of_isSeparable` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `isSeparable` `mem_separableClosure_iff`

---

← Back to Index