Basic

📁 Source: Mathlib/FieldTheory/PurelyInseparable/Basic.lean

Statistics

Metric	Count
Definitions `IsPurelyInseparable`, `perfectClosure`, `instUniqueAlgHomOfIsPurelyInseparable`, `instUniqueEmbOfIsPurelyInseparable`	4
Theorems `isPurelyInseparable`, `isPurelyInseparable_iff`, `isPurelyInseparable_of_isSepClosed`, `isSepClosed`, `cardinal_separableClosure`, `finSepDegree_eq`, `finSepDegree_mul_finInsepDegree`, `eq_bot_of_isPurelyInseparable_of_isSeparable`, `isPurelyInseparable_bot`, `isPurelyInseparable_tower_bot`, `isPurelyInseparable_tower_top`, `bijective_algebraMap_of_isSeparable`, `bijective_comp_algebraMap`, `bijective_restrictDomain`, `exists_pow_mem_range_tensorProduct`, `exists_pow_pow_mem_range_tensorProduct_of_expChar`, `finInsepDegree_eq`, `finSepDegree_eq_one`, `finrank_eq_pow`, `injective_comp_algebraMap`, `injective_restrictDomain`, `insepDegree_eq`, `inseparable`, `inseparable'`, `instNonemptyAlgHomOfPerfectField`, `isAlgebraic`, `isIntegral`, `isIntegral'`, `minpoly_eq_X_pow_sub_C`, `minpoly_eq_X_sub_C_pow`, `natSepDegree_eq_one`, `normal`, `of_injective_comp_algebraMap`, `pow_mem`, `sepDegree_eq_one`, `surjective_algebraMap_of_isSeparable`, `tower_bot`, `tower_top`, `trans`, `eq_bot_of_isPurelyInseparable_of_isSeparable`, `mem_perfectClosure_iff`, `eq_separableClosure`, `eq_separableClosure_iff`, `finInsepDegree_eq_pow`, `instSubsingletonAlgHomOfIsPurelyInseparable`, `isPurelyInseparable_iff`, `isPurelyInseparable_iff_fd_isPurelyInseparable`, `isPurelyInseparable_iff_finSepDegree_eq_one`, `isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C`, `isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow`, `isPurelyInseparable_iff_natSepDegree_eq_one`, `isPurelyInseparable_iff_pow_mem`, `isPurelyInseparable_of_finSepDegree_eq_one`, `isPurelyInseparable_self`, `isSepClosed_iff_isPurelyInseparable_algebraicClosure`, `isSeparable_iff_finInsepDegree_eq_one`, `adjoin_eq_of_isAlgebraic`, `adjoin_eq_of_isAlgebraic_of_isSeparable`, `eq_bot_iff`, `eq_bot_of_isPurelyInseparable`, `isPurelyInseparable`, `separableClosure_le`, `separableClosure_le_iff`	63
Total	67

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPurelyInseparable` 📖	mathematical	—	`IsPurelyInseparable`	—	`isIntegral_algEquiv` `IsPurelyInseparable.isIntegral'` `IsPurelyInseparable.inseparable` `minpoly.algEquiv_eq` `IsSeparable.eq_1`
`isPurelyInseparable_iff` 📖	mathematical	—	`IsPurelyInseparable`	—	`isPurelyInseparable`

Algebra.IsAlgebraic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPurelyInseparable_of_isSepClosed` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`isIntegral` `minpoly.mem_range_of_degree_eq_one` `IsSepClosed.degree_eq_one_of_irreducible` `minpoly.irreducible` `instIsDomain` `Algebra.IsIntegral.isIntegral`
`isSepClosed` 📖	mathematical	—	`IsSepClosed`	—	`trans` `AlgebraicClosure.instIsScalarTower` `IsScalarTower.right` `IsDomain.to_noZeroDivisors` `instIsDomain` `AlgebraicClosure.isAlgebraic` `isSepClosed_iff_isPurelyInseparable_algebraicClosure` `AlgebraicClosure.instIsAlgClosureOfIsAlgebraic` `Algebra.IsSeparable.isAlgebraic` `EuclideanDomain.toNontrivial` `Algebra.isSeparable_self` `IsPurelyInseparable.tower_top` `isPurelyInseparable_of_isSepClosed`

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finSepDegree_eq` 📖	mathematical	—	`finSepDegree` `DFunLike.coe` `MonoidWithZeroHom` `Cardinal` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Cardinal.commSemiring` `Nat.instMulZeroOneClass` `MonoidWithZeroHom.funLike` `Cardinal.toNat` `sepDegree`	—	`IsScalarTower.left` `finSepDegree_mul_finSepDegree_of_isAlgebraic` `IntermediateField.isScalarTower_mid'` `IntermediateField.isAlgebraic_tower_top` `mul_one` `IsPurelyInseparable.finSepDegree_eq_one` `separableClosure.isPurelyInseparable` `finSepDegree_eq_finrank_of_isSeparable` `separableClosure.isSeparable`
`finSepDegree_mul_finInsepDegree` 📖	mathematical	—	`finSepDegree` `finInsepDegree` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`sepDegree_mul_insepDegree` `finSepDegree_eq` `Cardinal.toNat_mul` `finInsepDegree.eq_1` `Module.finrank_of_infinite_dimensional` `Algebra.IsAlgebraic.of_finite` `EuclideanDomain.toNontrivial` `Algebra.IsAlgebraic.trans` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `separableClosure.isAlgebraic` `SubsemiringClass.nontrivial` `MulZeroClass.mul_zero`

Field.Emb

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cardinal_separableClosure` 📖	mathematical	—	`Field.Emb` `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` `Equiv.cardinal_eq` `IntermediateField.isScalarTower_mid'` `IntermediateField.isAlgebraic_tower_top` `Cardinal.mk_prod` `Cardinal.mk_eq_one` `instSubsingletonAlgHomOfIsPurelyInseparable` `separableClosure.isPurelyInseparable` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsPurelyInseparable.instNonemptyAlgHomOfPerfectField` `IsAlgClosed.perfectField` `AlgebraicClosure.isAlgClosed` `Cardinal.lift_one` `mul_one` `Cardinal.lift_id`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_of_isPurelyInseparable_of_isSeparable` 📖	mathematical	—	`Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IsScalarTower.left` `bot_unique` `IsPurelyInseparable.surjective_algebraMap_of_isSeparable` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass`
`isPurelyInseparable_bot` 📖	mathematical	—	`IsPurelyInseparable` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `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`	—	`AlgEquiv.isPurelyInseparable` `IsScalarTower.left` `isPurelyInseparable_self`
`isPurelyInseparable_tower_bot` 📖	mathematical	—	`IsPurelyInseparable` `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`	—	`IsPurelyInseparable.tower_bot` `IsScalarTower.left` `isScalarTower_mid'`
`isPurelyInseparable_tower_top` 📖	mathematical	—	`IsPurelyInseparable` `IntermediateField` `SetLike.instMembership` `instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `DivisionRing.toRing` `Field.toDivisionRing` `instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield`	—	`IsPurelyInseparable.tower_top` `IsScalarTower.left` `isScalarTower_mid'`

IsPurelyInseparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_algebraMap_of_isSeparable` 📖	mathematical	—	`Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`FaithfulSMul.algebraMap_injective` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `surjective_algebraMap_of_isSeparable`
`bijective_comp_algebraMap` 📖	mathematical	—	`Function.Bijective` `RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.comp` `algebraMap`	—	`injective_comp_algebraMap` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `instNonemptyAlgHomOfPerfectField` `AlgHom.comp_algebraMap`
`bijective_restrictDomain` 📖	mathematical	—	`Function.Bijective` `AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `AlgHom.restrictDomain`	—	`injective_restrictDomain` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `instNonemptyAlgHomOfPerfectField` `IsScalarTower.of_algHom` `AlgHom.coe_ringHom_injective` `AlgHom.comp_algebraMap`
`exists_pow_mem_range_tensorProduct` 📖	mathematical	—	`TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subring` `Algebra.TensorProduct.instRing` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `algebraMap` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Algebra.to_smulCommClass` `exists_pow_pow_mem_range_tensorProduct_of_expChar` `ringExpChar.expChar` `instIsDomain` `pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `expChar_is_prime_or_one`
`exists_pow_pow_mem_range_tensorProduct_of_expChar` 📖	mathematical	—	`TensorProduct` `Semifield.toCommSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subring` `Algebra.TensorProduct.instRing` `CommRing.toRing` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `algebraMap` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `Algebra.id` `Algebra.to_smulCommClass` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Algebra.to_smulCommClass` `Zero.instNonempty` `expChar_is_prime_or_one` `TensorProduct.induction_on` `TensorProduct.zero_tmul` `pow_zero` `pow_one` `pow_mem` `instIsDomain` `IsScalarTower.right` `Algebra.TensorProduct.tmul_mul_tmul` `mul_one` `one_mul` `Algebra.TensorProduct.tmul_pow` `Subring.mul_mem` `IsScalarTower.algebraMap_apply` `TensorProduct.isScalarTower_left` `Algebra.TensorProduct.algebraMap_apply` `Algebra.TensorProduct.tmul_one_eq_one_tmul` `expChar_of_injective_ringHom` `RingHom.injective` `DivisionRing.isSimpleRing` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `charZero_of_expChar_one'` `EuclideanDomain.toNontrivial` `Algebra.TensorProduct.includeLeft_surjective` `surjective_algebraMap_of_isSeparable` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `Normal.toIsAlgebraic` `normal` `PerfectField.ofCharZero`
`finInsepDegree_eq` 📖	mathematical	—	`Field.finInsepDegree` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring`	—	`insepDegree_eq`
`finSepDegree_eq_one` 📖	mathematical	—	`Field.finSepDegree`	—	`Nat.card_unique` `instNonemptyAlgHomOfPerfectField` `IsAlgClosed.perfectField` `AlgebraicClosure.isAlgClosed` `instSubsingletonAlgHomOfIsPurelyInseparable` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain`
`finrank_eq_pow` 📖	mathematical	—	`Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `Monoid.toNatPow` `Nat.instMonoid`	—	`pow_zero` `IsScalarTower.left` `IntermediateField.finrank_bot` `IntermediateField.finrank_top'` `SetLike.exists_of_lt` `instIsConcreteLE` `lt_of_le_of_ne` `bot_le` `minpoly_eq_X_pow_sub_C` `IntermediateField.adjoin.finrank` `Algebra.IsIntegral.isIntegral` `isIntegral` `Polynomial.natDegree_sub_C` `Polynomial.natDegree_X_pow` `EuclideanDomain.toNontrivial` `Module.finrank_mul_finrank` `IntermediateField.isScalarTower_mid'` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Module.Free.of_divisionRing` `Module.finrank_pos` `IntermediateField.finiteDimensional_right` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IntermediateField.finrank_adjoin_simple_eq_one_iff` `le_antisymm` `LT.lt.ne'` `IntermediateField.finiteDimensional_left` `IntermediateField.expChar` `IntermediateField.isPurelyInseparable_tower_top` `pow_add` `IntermediateField.finrank_bot'`
`injective_comp_algebraMap` 📖	mathematical	—	`RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Semifield.toCommSemiring` `RingHom.comp` `algebraMap`	—	`RingHom.ext` `pow_mem` `instIsDomain` `ringExpChar.expChar` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `expChar_of_injective_ringHom` `RingHom.injective` `DivisionRing.isSimpleRing` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`injective_restrictDomain` 📖	mathematical	—	`AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `CommRing.toCommSemiring` `AlgHom.restrictDomain`	—	`AlgHom.coe_ringHom_injective` `injective_comp_algebraMap` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`insepDegree_eq` 📖	mathematical	—	`Field.insepDegree` `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.insepDegree.eq_1` `separableClosure.eq_bot_of_isPurelyInseparable` `IntermediateField.rank_bot'`
`inseparable` 📖	mathematical	`IsSeparable`	`Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `CommRing.toRing` `algebraMap` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`inseparable'`
`inseparable'` 📖	mathematical	`IsSeparable`	`Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `CommRing.toRing` `algebraMap` `CommRing.toCommSemiring` `Ring.toSemiring`	—	—
`instNonemptyAlgHomOfPerfectField` 📖	mathematical	—	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IntermediateField.nonempty_algHom_of_splits` `isIntegral'` `ExpChar.exists` `instIsDomain` `PerfectField.splits_of_natSepDegree_eq_one` `minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C` `minpoly_eq_X_pow_sub_C`
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic`	—	`Algebra.IsIntegral.isAlgebraic` `isIntegral`
`isIntegral` 📖	mathematical	—	`Algebra.IsIntegral`	—	—
`isIntegral'` 📖	mathematical	—	`IsIntegral`	—	`Algebra.IsIntegral.isIntegral` `isIntegral`
`minpoly_eq_X_pow_sub_C` 📖	mathematical	—	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C`
`minpoly_eq_X_sub_C_pow` 📖	mathematical	—	`Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Nat.instMonoid`	—	`isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow`
`natSepDegree_eq_one` 📖	mathematical	—	`Polynomial.natSepDegree` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`isPurelyInseparable_iff_natSepDegree_eq_one`
`normal` 📖	mathematical	—	`Normal`	—	`isAlgebraic` `EuclideanDomain.toNontrivial` `minpoly_eq_X_sub_C_pow` `ringExpChar.expChar` `instIsDomain` `Polynomial.Splits.pow` `Polynomial.Splits.X_sub_C`
`of_injective_comp_algebraMap` 📖	mathematical	`RingHom` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `RingHom.comp` `algebraMap`	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`isPurelyInseparable_iff_finSepDegree_eq_one` `Field.finSepDegree.eq_1` `Nat.card_eq_one_iff_unique` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `AlgebraicClosure.isAlgebraic` `DFunLike.ext'` `Function.Injective.comp_left` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHom.ext` `AlgHom.commutes`
`pow_mem` 📖	mathematical	—	`Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `DivisionRing.toRing` `Field.toDivisionRing` `algebraMap` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`isPurelyInseparable_iff_pow_mem`
`sepDegree_eq_one` 📖	mathematical	—	`Field.sepDegree` `Cardinal` `Cardinal.instOne`	—	`Field.sepDegree.eq_1` `separableClosure.eq_bot_of_isPurelyInseparable` `IsScalarTower.left` `IntermediateField.rank_bot`
`surjective_algebraMap_of_isSeparable` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`inseparable` `Algebra.IsSeparable.isSeparable`
`tower_bot` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`IsIntegral.tower_bot_of_field` `EuclideanDomain.toNontrivial` `isIntegral'` `inseparable` `minpoly.algebraMap_eq` `RingHom.injective` `DivisionRing.isSimpleRing` `IsSeparable.eq_1` `IsScalarTower.algebraMap_apply`
`tower_top` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`ExpChar.exists` `instIsDomain` `isPurelyInseparable_iff_pow_mem` `expChar_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `IsScalarTower.algebraMap_apply`
`trans` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`ExpChar.exists` `instIsDomain` `isPurelyInseparable_iff_pow_mem` `expChar_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `IsScalarTower.algebraMap_apply` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `pow_mul` `pow_add`

Subalgebra

Definitions

Name	Category	Theorems
`perfectClosure` 📖	CompOp	1 math math: `mem_perfectClosure_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_of_isPurelyInseparable_of_isSeparable` 📖	mathematical	—	`Bot.bot` `Subalgebra` `CommRing.toCommSemiring` `Ring.toSemiring` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`bot_unique` `IsPurelyInseparable.surjective_algebraMap_of_isSeparable`
`mem_perfectClosure_iff` 📖	mathematical	—	`Subalgebra` `CommSemiring.toSemiring` `SetLike.instMembership` `instSetLike` `perfectClosure` `Subsemiring` `Semiring.toNonAssocSemiring` `Subsemiring.instSetLike` `RingHom.rangeS` `algebraMap` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	—

(root)

Definitions

Name	Category	Theorems
`IsPurelyInseparable` 📖	CompData	33 math math: `IsPurelyInseparable.instOfHasExponent`, `isPurelyInseparable_iff_fd_isPurelyInseparable`, `isPurelyInseparable_iff_pow_mem`, `IntermediateField.isPurelyInseparable_tower_bot`, `eq_separableClosure_iff`, `isPurelyInseparable_iff_natSepDegree_eq_one`, `AlgEquiv.isPurelyInseparable`, `IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem`, `isPurelyInseparable_self`, `IsPRadical.isPurelyInseparable`, `isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow`, `IsPurelyInseparable.trans`, `isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C`, `IsPurelyInseparable.tower_bot`, `isPurelyInseparable_iff_perfectClosure_eq_top`, `isPurelyInseparable_iff`, `isPurelyInseparable_iff_finSepDegree_eq_one`, `isPurelyInseparable_of_finSepDegree_eq_one`, `IntermediateField.isPurelyInseparable_bot`, `le_perfectClosure_iff`, `AlgEquiv.isPurelyInseparable_iff`, `isSepClosed_iff_isPurelyInseparable_algebraicClosure`, `IsPurelyInseparable.of_injective_comp_algebraMap`, `separableClosure_le_iff`, `IntermediateField.isPurelyInseparable_tower_top`, `Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed`, `IntermediateField.isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one`, `separableClosure.eq_bot_iff`, `IntermediateField.isPurelyInseparable_sup`, `separableClosure.isPurelyInseparable`, `IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem`, `perfectClosure.isPurelyInseparable`, `IsPurelyInseparable.tower_top`
`instUniqueAlgHomOfIsPurelyInseparable` 📖	CompOp	—
`instUniqueEmbOfIsPurelyInseparable` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_separableClosure` 📖	mathematical	—	`separableClosure`	—	`IsScalarTower.left` `le_antisymm` `le_separableClosure` `separableClosure_le`
`eq_separableClosure_iff` 📖	mathematical	—	`separableClosure` `Algebra.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` `IsPurelyInseparable` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring`	—	`IsScalarTower.left` `separableClosure.isSeparable` `separableClosure.isPurelyInseparable` `eq_separableClosure`
`finInsepDegree_eq_pow` 📖	mathematical	—	`Field.finInsepDegree` `Monoid.toNatPow` `Nat.instMonoid`	—	`IsPurelyInseparable.finrank_eq_pow` `IntermediateField.expChar` `separableClosure.isPurelyInseparable` `Algebra.IsAlgebraic.of_finite` `EuclideanDomain.toNontrivial` `IntermediateField.finiteDimensional_right`
`instSubsingletonAlgHomOfIsPurelyInseparable` 📖	mathematical	—	`AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`AlgHom.coe_ringHom_injective` `IsPurelyInseparable.injective_comp_algebraMap` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap`
`isPurelyInseparable_iff` 📖	mathematical	—	`IsPurelyInseparable` `IsIntegral` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `CommRing.toRing` `algebraMap` `CommRing.toCommSemiring` `Ring.toSemiring`	—	`IsPurelyInseparable.isIntegral'` `IsPurelyInseparable.inseparable'`
`isPurelyInseparable_iff_fd_isPurelyInseparable` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `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` `IsPurelyInseparable.tower_bot` `IntermediateField.isScalarTower_mid'` `isPurelyInseparable_iff` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `IsPurelyInseparable.inseparable'` `IntermediateField.adjoin.finiteDimensional` `IntermediateField.minpoly_eq` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass`
`isPurelyInseparable_iff_finSepDegree_eq_one` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Field.finSepDegree`	—	`IsPurelyInseparable.finSepDegree_eq_one` `isPurelyInseparable_of_finSepDegree_eq_one`
`isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `minpoly` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.instSub` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Nat.instMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	—	`minpoly.natSepDegree_eq_one_iff_eq_X_pow_sub_C` `instIsDomain`
`isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `algebraMap` `minpoly` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Nat.instMonoid`	—	`minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_pow` `instIsDomain`
`isPurelyInseparable_iff_natSepDegree_eq_one` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.natSepDegree` `minpoly`	—	`ExpChar.exists` `instIsDomain` `isPurelyInseparable_iff_pow_mem` `minpoly.natSepDegree_eq_one_iff_pow_mem`
`isPurelyInseparable_iff_pow_mem` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `DivisionRing.toRing` `Field.toDivisionRing` `algebraMap` `Semifield.toCommSemiring` `Field.toSemifield` `Ring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`isPurelyInseparable_iff` `Irreducible.hasSeparableContraction` `minpoly.irreducible` `instIsDomain` `Polynomial.Separable.of_dvd` `minpoly.dvd` `Polynomial.expand_aeval` `minpoly.aeval` `minpoly.natSepDegree_eq_one_iff_pow_mem` `by_contra` `minpoly.eq_zero` `Polynomial.natSepDegree_zero` `minpoly.natDegree_eq_one_iff` `IsDomain.toNontrivial` `Polynomial.Separable.natSepDegree_eq_natDegree`
`isPurelyInseparable_of_finSepDegree_eq_one` 📖	mathematical	`Field.finSepDegree`	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`isPurelyInseparable_iff` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `IsScalarTower.left` `Field.finSepDegree_mul_finSepDegree_of_isAlgebraic` `IntermediateField.isScalarTower_mid'` `IntermediateField.isAlgebraic_tower_top` `IntermediateField.finrank_eq_one_iff` `IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff` `Algebra.IsAlgebraic.isAlgebraic` `mul_eq_one` `Unique.instSubsingleton` `IntermediateField.mem_adjoin_simple_self` `Field.finSepDegree_eq_zero_of_transcendental` `Algebra.transcendental_iff_not_isAlgebraic`
`isPurelyInseparable_self` 📖	mathematical	—	`IsPurelyInseparable` `CommRing.toRing` `Algebra.id` `CommRing.toCommSemiring`	—	`Algebra.IsIntegral.of_finite` `Module.Finite.self`
`isSepClosed_iff_isPurelyInseparable_algebraicClosure` 📖	mathematical	—	`IsSepClosed` `IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed` `IsAlgClosure.isAlgebraic` `IsSepClosed.separableClosure_eq_bot_iff` `IsSepClosed.of_isAlgClosed` `IsAlgClosure.isAlgClosed` `separableClosure.eq_bot_iff`
`isSeparable_iff_finInsepDegree_eq_one` 📖	mathematical	—	`Algebra.IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Field.finInsepDegree`	—	`separableClosure.eq_top_iff` `IntermediateField.finrank_eq_one_iff_eq_top` `Field.finInsepDegree.eq_1`
`separableClosure_le` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `separableClosure`	—	`IsPurelyInseparable.inseparable'` `IsSeparable.tower_top` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `mem_separableClosure_iff`
`separableClosure_le_iff` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `separableClosure` `IsPurelyInseparable` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield`	—	`IsPurelyInseparable.tower_top` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `IsScalarTower.of_algebraMap_eq` `separableClosure.isPurelyInseparable` `separableClosure_le`

separableClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_eq_of_isAlgebraic` 📖	mathematical	—	`IntermediateField.adjoin` `SetLike.coe` `IntermediateField` `IntermediateField.instSetLike` `separableClosure`	—	`IsScalarTower.left` `adjoin_eq_of_isAlgebraic_of_isSeparable` `IntermediateField.isScalarTower` `isSeparable` `IntermediateField.lift_adjoin` `IntermediateField.lift_top` `IsScalarTower.of_algebraMap_eq` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `map_eq_of_separableClosure_eq_bot` `separableClosure_eq_bot` `Set.image_congr`
`adjoin_eq_of_isAlgebraic_of_isSeparable` 📖	mathematical	—	`IntermediateField.adjoin` `SetLike.coe` `IntermediateField` `IntermediateField.instSetLike` `separableClosure` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`top_unique` `Algebra.isSeparable_tower_top_of_isSeparable` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IntermediateField.subset_adjoin` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.of_algebraMap_eq` `Algebra.IsAlgebraic.trans` `IsDomain.to_noZeroDivisors` `instIsDomain` `Algebra.IsSeparable.isAlgebraic` `EuclideanDomain.toNontrivial` `isPurelyInseparable` `IsPurelyInseparable.tower_top` `IsPurelyInseparable.surjective_algebraMap_of_isSeparable`
`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` `IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`isPurelyInseparable_iff` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `mem_separableClosure_iff` `eq_bot_of_isPurelyInseparable`
`eq_bot_of_isPurelyInseparable` 📖	mathematical	—	`separableClosure` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`bot_unique` `IsPurelyInseparable.inseparable` `mem_separableClosure_iff`
`isPurelyInseparable` 📖	mathematical	—	`IsPurelyInseparable` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `separableClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.toField` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.instAlgebraSubtypeMem` `Ring.toSemiring` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield`	—	`isPurelyInseparable_iff` `IsAlgebraic.isIntegral` `IsAlgebraic.tower_top` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `Algebra.IsAlgebraic.isAlgebraic` `IntermediateField.mem_adjoin_simple_self` `mem_separableClosure_iff` `IntermediateField.isSeparable_of_mem_isSeparable` `Algebra.IsSeparable.trans` `IntermediateField.instIsScalarTowerSubtypeMem_1` `IsScalarTower.right` `isSeparable` `IntermediateField.isSeparable_adjoin_simple_iff_isSeparable`

---

← Back to Index