Documentation Verification Report

PerfectClosure

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

Statistics

Metric	Count
Definitions `perfectClosure`, `mapPowExpCharPowOfIsSeparable`, `PerfectClosure`, `perfectClosure`, `algEquivOfAlgEquiv`	5
Theorems `span_map_pow_expChar_pow_eq_top_of_isSeparable`, `adjoin_eq_adjoin_pow_expChar_of_isSeparable`, `adjoin_eq_adjoin_pow_expChar_of_isSeparable'`, `adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable`, `adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable'`, `adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable`, `adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable'`, `adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable`, `adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable'`, `isPurelyInseparable_adjoin_iff_pow_mem`, `isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one`, `isPurelyInseparable_adjoin_simple_iff_pow_mem`, `isPurelyInseparable_iSup`, `isPurelyInseparable_sup`, `map_pow_expChar_pow_of_isSeparable`, `map_pow_expChar_pow_of_isSeparable'`, `isPurelyInseparable_iff_perfectClosure_eq_top`, `le_perfectClosure`, `le_perfectClosure_iff`, `map_mem_perfectClosure_iff`, `mem_perfectClosure_iff`, `mem_perfectClosure_iff_natSepDegree_eq_one`, `mem_perfectClosure_iff_pow_mem`, `frobenius_of_isSeparable`, `iterateFrobenius_of_isSeparable`, `comap_eq_of_algHom`, `eq_bot_of_isSeparable`, `isAlgebraic`, `isPurelyInseparable`, `map_eq_of_algEquiv`, `map_le_of_algHom`, `perfectField`, `perfectRing`, `perfectField_iff_isSeparable_algebraicClosure`, `perfectField_of_isSeparable_of_perfectField_top`, `perfectField_of_perfectClosure_eq_bot`, `separableClosure_inf_perfectClosure`	37
Total	42

AlgEquiv

Definitions

Name	Category	Theorems
`perfectClosure` 📖	CompOp	—

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`span_map_pow_expChar_pow_eq_top_of_isSeparable` 📖	mathematical	`Submodule.span` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `Set.range` `Top.top` `Submodule` `Submodule.instTop`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`Algebra.top_toSubmodule` `IntermediateField.top_toSubalgebra` `IntermediateField.adjoin_univ` `IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable'` `IntermediateField.adjoin_toSubalgebra_of_isAlgebraic` `Algebra.IsAlgebraic.isAlgebraic` `Algebra.IsSeparable.isAlgebraic` `EuclideanDomain.toNontrivial` `Set.image_univ` `Algebra.adjoin_eq_span` `MonoidHom.instMonoidHomClass` `Submonoid.closure_eq` `mul_pow` `LE.le.antisymm` `Submodule.span_mono` `Set.range_comp_subset_range` `Submodule.span_le` `Set.range_comp` `expChar_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `Submodule.image_span_subset_span`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_eq_adjoin_pow_expChar_of_isSeparable` 📖	mathematical	—	`adjoin` `Set.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`IsScalarTower.left` `adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable` `pow_one`
`adjoin_eq_adjoin_pow_expChar_of_isSeparable'` 📖	mathematical	—	`adjoin` `Set.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable'` `pow_one`
`adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable` 📖	mathematical	—	`adjoin` `Set.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Nat.instMonoid`	—	`IsScalarTower.left` `adjoin_le_iff` `pow_mem` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `subset_adjoin` `isScalarTower_mid'` `restrictScalars_bot_eq_self` `eq_bot_of_isPurelyInseparable_of_isSeparable` `extendScalars_adjoin` `isPurelyInseparable_adjoin_iff_pow_mem` `expChar` `Algebra.isSeparable_tower_top_of_isSeparable` `IsScalarTower.of_algHom`
`adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable'` 📖	mathematical	—	`adjoin` `Set.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Nat.instMonoid`	—	`adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable` `Algebra.isSeparable_tower_bot_of_isSeparable` `IsScalarTower.left` `EuclideanDomain.toNontrivial` `isScalarTower_mid'`
`adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`adjoin` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable` `pow_one`
`adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable'` 📖	mathematical	—	`adjoin` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable'` `pow_one`
`adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`adjoin` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Nat.instMonoid`	—	`Set.image_singleton` `adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable` `IsScalarTower.left` `isSeparable_adjoin_simple_iff_isSeparable`
`adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable'` 📖	mathematical	—	`adjoin` `Set` `Set.instSingletonSet` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Nat.instMonoid`	—	`Set.image_singleton` `adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable` `isSeparable_tower_bot`
`isPurelyInseparable_adjoin_iff_pow_mem` 📖	mathematical	—	`IsPurelyInseparable` `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` `Subring` `Subring.instSetLike` `RingHom.range` `algebraMap` `Monoid.toNatPow` `Nat.instMonoid`	—	`IsScalarTower.left` `mem_perfectClosure_iff_pow_mem`
`isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one` 📖	mathematical	—	`IsPurelyInseparable` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `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` `Polynomial.natSepDegree` `minpoly`	—	`IsScalarTower.left` `le_perfectClosure_iff` `adjoin_simple_le_iff` `mem_perfectClosure_iff_natSepDegree_eq_one`
`isPurelyInseparable_adjoin_simple_iff_pow_mem` 📖	mathematical	—	`IsPurelyInseparable` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Set` `Set.instSingletonSet` `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` `Subring` `Subring.instSetLike` `RingHom.range` `algebraMap` `Monoid.toNatPow` `Nat.instMonoid`	—	`IsScalarTower.left` `le_perfectClosure_iff` `adjoin_simple_le_iff` `mem_perfectClosure_iff_pow_mem`
`isPurelyInseparable_iSup` 📖	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`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice`	—	`IsScalarTower.left` `iSup_le`
`isPurelyInseparable_sup` 📖	mathematical	—	`IsPurelyInseparable` `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_perfectClosure_iff` `sup_le`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_pow_expChar_pow_of_isSeparable` 📖	mathematical	`LinearIndependent` `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` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`linearIndependent_iff_finset_linearIndependent` `IntermediateField.subset_adjoin` `Finset.mem_image` `IsScalarTower.left` `of_comp` `map'` `IntermediateField.finiteDimensional_adjoin` `Finite.of_fintype` `Algebra.IsIntegral.isIntegral` `Algebra.IsAlgebraic.isIntegral` `Algebra.IsSeparable.isAlgebraic` `EuclideanDomain.toNontrivial` `IntermediateField.isSeparable_tower_bot` `LinearMap.ker_eq_bot_of_injective` `RingHom.injective` `DivisionRing.isSimpleRing`
`map_pow_expChar_pow_of_isSeparable'` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `LinearIndependent` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule` `Semifield.toCommSemiring`	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`IntermediateField.subset_adjoin` `IsScalarTower.left` `of_comp` `map'` `map_pow_expChar_pow_of_isSeparable` `IntermediateField.isSeparable_adjoin_iff_isSeparable` `LinearMap.ker_eq_bot_of_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial`

Module.Basis

Definitions

Name	Category	Theorems
`mapPowExpCharPowOfIsSeparable` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`PerfectClosure` 📖	CompOp	22 math math: `PerfectClosure.mk_mul_mk`, `PerfectClosure.frobenius_mk`, `PerfectClosure.instCharP`, `PerfectClosure.instPerfectRing`, `PerfectClosure.instNontrivialOfIsReduced`, `PerfectClosure.mk_add_mk`, `PerfectClosure.neg_mk`, `PerfectClosure.natCast_eq_iff`, `PerfectClosure.of_apply`, `PerfectClosure.intCast`, `PerfectClosure.mk_zero_right`, `PerfectClosure.mk_surjective`, `PerfectClosure.instPerfectField`, `PerfectClosure.isPRadical`, `PerfectClosure.zero_def`, `PerfectClosure.iterate_frobenius_mk`, `PerfectClosure.instReduced`, `PerfectClosure.mk_inv`, `PerfectClosure.mk_pow`, `PerfectClosure.mk_zero`, `PerfectClosure.one_def`, `PerfectClosure.natCast`
`perfectClosure` 📖	CompOp	16 math math: `mem_perfectClosure_iff_natSepDegree_eq_one`, `perfectClosure.map_le_of_algHom`, `mem_perfectClosure_iff_pow_mem`, `map_mem_perfectClosure_iff`, `mem_perfectClosure_iff`, `le_perfectClosure`, `separableClosure_inf_perfectClosure`, `isPurelyInseparable_iff_perfectClosure_eq_top`, `le_perfectClosure_iff`, `perfectClosure.isAlgebraic`, `perfectClosure.perfectField`, `perfectClosure.eq_bot_of_isSeparable`, `perfectClosure.map_eq_of_algEquiv`, `perfectClosure.perfectRing`, `perfectClosure.comap_eq_of_algHom`, `perfectClosure.isPurelyInseparable`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPurelyInseparable_iff_perfectClosure_eq_top` 📖	mathematical	—	`IsPurelyInseparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `perfectClosure` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`isPurelyInseparable_iff_pow_mem` `instIsDomain` `ringExpChar.expChar` `top_unique` `Eq.ge`
`le_perfectClosure` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `perfectClosure`	—	`IsScalarTower.left` `isPurelyInseparable_iff_pow_mem` `instIsDomain` `ringExpChar.expChar` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass`
`le_perfectClosure_iff` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `perfectClosure` `IsPurelyInseparable` `SetLike.instMembership` `IntermediateField.instSetLike` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `isPurelyInseparable_iff_pow_mem` `instIsDomain` `ringExpChar.expChar` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `le_perfectClosure`
`map_mem_perfectClosure_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `perfectClosure` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.funLike`	—	`RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `AlgHom.commutes` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`mem_perfectClosure_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `perfectClosure` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `Subring.instSetLike` `RingHom.range` `algebraMap` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid` `ringExpChar` `Semiring.toNonAssocSemiring`	—	—
`mem_perfectClosure_iff_natSepDegree_eq_one` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `perfectClosure` `Polynomial.natSepDegree` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`mem_perfectClosure_iff` `minpoly.natSepDegree_eq_one_iff_pow_mem` `instIsDomain` `ringExpChar.expChar`
`mem_perfectClosure_iff_pow_mem` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `perfectClosure` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `Subring.instSetLike` `RingHom.range` `algebraMap` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid`	—	`mem_perfectClosure_iff` `ringExpChar.eq`
`perfectField_iff_isSeparable_algebraicClosure` 📖	mathematical	—	`PerfectField` `Algebra.IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `IsSepClosure.separable` `IsSepClosure.of_isAlgClosure_of_perfectField` `perfectField_of_isSeparable_of_perfectField_top` `IsAlgClosed.perfectField` `IsAlgClosure.isAlgClosed`
`perfectField_of_isSeparable_of_perfectField_top` 📖	mathematical	—	`PerfectField`	—	`perfectField_of_perfectClosure_eq_bot` `perfectClosure.eq_bot_of_isSeparable`
`perfectField_of_perfectClosure_eq_bot` 📖	mathematical	`perfectClosure` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`PerfectField`	—	`PerfectRing.toPerfectField` `ringExpChar.expChar` `instIsDomain` `PerfectRing.ofSurjective` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `expChar_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `surjective_frobenius` `PerfectField.toPerfectRing` `pow_one` `frobenius_def` `ringExpChar.eq` `RingHom.map_frobenius`
`separableClosure_inf_perfectClosure` 📖	mathematical	—	`IntermediateField` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `separableClosure` `perfectClosure` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable` `IsScalarTower.left` `le_perfectClosure_iff` `inf_le_right` `le_separableClosure_iff` `inf_le_left`

minpoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`frobenius_of_isSeparable` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`minpoly` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.instFunLike` `frobenius` `Polynomial.map`	—	`iterateFrobenius_one` `iterateFrobenius_of_isSeparable`
`iterateFrobenius_of_isSeparable` 📖	mathematical	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`minpoly` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.instFunLike` `iterateFrobenius` `Polynomial.map`	—	`IsSeparable.isIntegral` `IsIntegral.pow` `Polynomial.eq_of_monic_of_dvd_of_natDegree_le` `monic` `Polynomial.Monic.map` `dvd` `aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Polynomial.map_aeval_eq_aeval_map` `RingHom.iterateFrobenius_comm` `Polynomial.natDegree_map_eq_of_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `IsScalarTower.left` `IntermediateField.adjoin.finrank` `IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable` `iterateFrobenius_def` `le_refl`

perfectClosure

Definitions

Name	Category	Theorems
`algEquivOfAlgEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_eq_of_algHom` 📖	mathematical	—	`IntermediateField.comap` `perfectClosure`	—	`IntermediateField.ext` `map_mem_perfectClosure_iff`
`eq_bot_of_isSeparable` 📖	mathematical	—	`perfectClosure` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable` `isPurelyInseparable` `Algebra.isSeparable_tower_bot_of_isSeparable` `IsScalarTower.left` `EuclideanDomain.toNontrivial` `IntermediateField.isScalarTower_mid'`
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `perfectClosure` `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.isAlgebraic` `IsScalarTower.left` `EuclideanDomain.toNontrivial` `isPurelyInseparable`
`isPurelyInseparable` 📖	mathematical	—	`IsPurelyInseparable` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `perfectClosure` `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` `isPurelyInseparable_iff_pow_mem` `instIsDomain` `ringExpChar.expChar` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass`
`map_eq_of_algEquiv` 📖	mathematical	—	`IntermediateField.map` `AlgEquiv.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `perfectClosure`	—	`LE.le.antisymm` `map_le_of_algHom` `map_mem_perfectClosure_iff` `Equiv.right_inv`
`map_le_of_algHom` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `IntermediateField.map` `perfectClosure`	—	`IntermediateField.map_le_iff_le_comap` `Eq.ge` `comap_eq_of_algHom`
`perfectField` 📖	mathematical	—	`PerfectField` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `perfectClosure` `IntermediateField.toField`	—	`PerfectRing.toPerfectField` `IntermediateField.expChar'` `ringExpChar.expChar` `instIsDomain` `perfectRing` `PerfectField.toPerfectRing`
`perfectRing` 📖	mathematical	—	`PerfectRing` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `perfectClosure` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.expChar'`	—	`PerfectRing.ofSurjective` `IntermediateField.expChar'` `isReduced_of_noZeroDivisors` `SubsemiringClass.noZeroDivisors` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsDomain.to_noZeroDivisors` `instIsDomain` `surjective_frobenius` `mem_perfectClosure_iff_pow_mem` `RingHom.expChar` `RingHom.injective` `DivisionRing.isSimpleRing` `EuclideanDomain.toNontrivial` `pow_succ'` `pow_mul` `frobenius_def` `pow_mem` `SubsemiringClass.toSubmonoidClass`

---

← Back to Index