Documentation Verification Report

GaloisClosure

📁 Source: Mathlib/FieldTheory/Galois/GaloisClosure.lean

Statistics

Metric	Count
Definitions `FiniteGaloisIntermediateField`, `adjoin`, `instCoeIntermediateField`, `instCoeSortType`, `instLattice`, `instMax`, `instMin`, `instOrderBot`, `instPartialOrder`, `toIntermediateField`	10
Theorems `adjoin_map`, `adjoin_simple_le_iff`, `adjoin_simple_map_algEquiv`, `adjoin_simple_map_algHom`, `adjoin_val`, `finiteDimensional`, `instFiniteDimensionalSubtypeMemIntermediateField`, `instFiniteDimensionalSubtypeMemIntermediateFieldMin`, `instFiniteDimensionalSubtypeMemIntermediateFieldMin_1`, `instIsGaloisSubtypeMemIntermediateField`, `instIsGaloisSubtypeMemIntermediateFieldMax`, `instIsGaloisSubtypeMemIntermediateFieldMin`, `instIsSeparableSubtypeMemIntermediateFieldMin`, `instIsSeparableSubtypeMemIntermediateFieldMin_1`, `isGalois`, `le_iff`, `mem_fixingSubgroup_iff`, `subset_adjoin`, `val_injective`	19
Total	29

FiniteGaloisIntermediateField

Definitions

Name	Category	Theorems
`adjoin` 📖	CompOp	7 math math: `subset_adjoin`, `InfiniteGalois.proj_adjoin_singleton_val`, `adjoin_map`, `adjoin_val`, `adjoin_simple_map_algEquiv`, `adjoin_simple_map_algHom`, `adjoin_simple_le_iff`
`instCoeIntermediateField` 📖	CompOp	—
`instCoeSortType` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	—
`instMin` 📖	CompOp	—
`instOrderBot` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	13 math math: `InfiniteGalois.toAlgEquivAux_eq_proj_of_mem`, `InfiniteGalois.mulEquivToLimit_symm_continuous`, `InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup`, `finGaloisGroupMap.map_id`, `InfiniteGalois.proj_adjoin_singleton_val`, `InfiniteGalois.toAlgEquivAux_eq_liftNormal`, `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `InfiniteGalois.mk_toAlgEquivAux`, `InfiniteGalois.algEquivToLimit_continuous`, `le_iff`, `InfiniteGalois.limitToAlgEquiv_symm_apply`, `finGaloisGroupMap.map_comp`, `adjoin_simple_le_iff`
`toIntermediateField` 📖	CompOp	14 math math: `instIsGaloisSubtypeMemIntermediateField`, `subset_adjoin`, `mem_fixingSubgroup_iff`, `InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois`, `InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup`, `isGalois`, `adjoin_val`, `finiteDimensional`, `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `instFiniteDimensionalSubtypeMemIntermediateField`, `InfiniteGalois.proj_of_le`, `val_injective`, `le_iff`, `adjoin_simple_le_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_map` 📖	mathematical	—	`adjoin` `Set.image` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.funLike` `Finite.Set.finite_image`	—	`val_injective` `Finite.Set.finite_image` `IsScalarTower.left` `IntermediateField.adjoin_map` `IntermediateField.normalClosure_map_eq` `IsGalois.to_normal`
`adjoin_simple_le_iff` 📖	mathematical	—	`FiniteGaloisIntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `adjoin` `Set` `Set.instSingletonSet` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `toIntermediateField`	—	`Finite.of_fintype` `IsScalarTower.left` `IsGalois.to_normal` `instIsGaloisSubtypeMemIntermediateField`
`adjoin_simple_map_algEquiv` 📖	mathematical	—	`adjoin` `Set` `Set.instSingletonSet` `DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton`	—	`adjoin_simple_map_algHom` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`adjoin_simple_map_algHom` 📖	mathematical	—	`adjoin` `Set` `Set.instSingletonSet` `DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgHom.funLike` `Finite.of_fintype` `Set.Elem` `Set.fintypeSingleton`	—	`Finite.Set.finite_image` `Finite.of_fintype` `Set.image_singleton` `adjoin.congr_simp` `adjoin_map`
`adjoin_val` 📖	mathematical	—	`toIntermediateField` `adjoin` `IntermediateField.normalClosure` `IntermediateField` `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` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	—
`finiteDimensional` 📖	mathematical	—	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `toIntermediateField` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `IntermediateField.toField` `IntermediateField.module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction`	—	—
`instFiniteDimensionalSubtypeMemIntermediateField` 📖	mathematical	—	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `toIntermediateField` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `IntermediateField.toField` `IntermediateField.module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction`	—	`finiteDimensional`
`instFiniteDimensionalSubtypeMemIntermediateFieldMin` 📖	mathematical	—	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `IntermediateField.toField` `IntermediateField.module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction`	—	`IsScalarTower.left` `FiniteDimensional.of_injective` `inf_le_left` `RingHom.injective` `DivisionRing.isSimpleRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instFiniteDimensionalSubtypeMemIntermediateFieldMin_1` 📖	mathematical	—	`FiniteDimensional` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `IntermediateField.toField` `IntermediateField.module'` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toModule` `Semifield.toDivisionSemiring` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction`	—	`IsScalarTower.left` `FiniteDimensional.of_injective` `inf_le_right` `RingHom.injective` `DivisionRing.isSimpleRing` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instIsGaloisSubtypeMemIntermediateField` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `toIntermediateField` `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`	—	`isGalois`
`instIsGaloisSubtypeMemIntermediateFieldMax` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `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` `IntermediateField.isSeparable_sup` `IsGalois.to_isSeparable` `IntermediateField.normal_sup` `IsGalois.to_normal`
`instIsGaloisSubtypeMemIntermediateFieldMin` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `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` `instIsSeparableSubtypeMemIntermediateFieldMin_1` `IsGalois.to_isSeparable` `IntermediateField.normal_inf` `IsGalois.to_normal`
`instIsSeparableSubtypeMemIntermediateFieldMin` 📖	mathematical	—	`Algebra.IsSeparable` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `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` `Algebra.IsSeparable.of_algHom` `inf_le_left`
`instIsSeparableSubtypeMemIntermediateFieldMin_1` 📖	mathematical	—	`Algebra.IsSeparable` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `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` `Algebra.IsSeparable.of_algHom` `inf_le_right`
`isGalois` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `toIntermediateField` `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_iff` 📖	mathematical	—	`FiniteGaloisIntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `IntermediateField` `IntermediateField.instPartialOrder` `toIntermediateField`	—	—
`mem_fixingSubgroup_iff` 📖	mathematical	—	`AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `IntermediateField.fixingSubgroup` `toIntermediateField` `DFunLike.coe` `MonoidHom` `IntermediateField` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike` `AlgEquiv.restrictNormalHom` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `IsGalois.to_normal` `instIsGaloisSubtypeMemIntermediateField` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`IsScalarTower.left` `IntermediateField.isScalarTower_mid'` `IsGalois.to_normal` `instIsGaloisSubtypeMemIntermediateField` `AlgEquiv.restrictNormalHom_apply`
`subset_adjoin` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `IntermediateField` `IntermediateField.instSetLike` `toIntermediateField` `adjoin`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `IntermediateField.subset_adjoin` `IntermediateField.le_normalClosure`
`val_injective` 📖	mathematical	—	`FiniteGaloisIntermediateField` `IntermediateField` `toIntermediateField`	—	`IsScalarTower.left`

(root)

Definitions

Name	Category	Theorems
`FiniteGaloisIntermediateField` 📖	CompData	14 math math: `InfiniteGalois.toAlgEquivAux_eq_proj_of_mem`, `InfiniteGalois.mulEquivToLimit_symm_continuous`, `InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup`, `finGaloisGroupMap.map_id`, `InfiniteGalois.proj_adjoin_singleton_val`, `InfiniteGalois.toAlgEquivAux_eq_liftNormal`, `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `InfiniteGalois.mk_toAlgEquivAux`, `FiniteGaloisIntermediateField.val_injective`, `InfiniteGalois.algEquivToLimit_continuous`, `FiniteGaloisIntermediateField.le_iff`, `InfiniteGalois.limitToAlgEquiv_symm_apply`, `finGaloisGroupMap.map_comp`, `FiniteGaloisIntermediateField.adjoin_simple_le_iff`

---

← Back to Index