Basic

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

Statistics

Metric	Count
Definitions `intermediateField`, `fixedField`, `algebra`, `smul`, `fixingSubgroup`, `fixingSubgroupEquiv`, `restrictRestrictAlgEquivMapHom`, `subgroupEquivAlgEquiv`, `IsGalois`, `galoisCoinsertionIntermediateFieldSubgroup`, `galoisInsertionIntermediateFieldSubgroup`, `intermediateFieldEquivSubgroup`, `normalAutEquivQuotient`	13
Theorems `transfer_galois`, `isCyclic`, `isGalois`, `isMulCommutative_galoisGroup`, `mem_intermediateField_iff`, `finrank_fixedField_eq_card`, `isScalarTower`, `fixedField_antitone`, `fixedField_bot`, `fixedField_le`, `fixingSubgroup_antitone`, `fixingSubgroup_bot`, `fixingSubgroup_fixedField`, `fixingSubgroup_le`, `fixingSubgroup_sup`, `fixingSubgroup_top`, `le_iff_le`, `mem_fixedField_iff`, `mem_fixingSubgroup_iff`, `restrictNormalHom_ker`, `restrictRestrictAlgEquivMapHom_apply`, `restrictRestrictAlgEquivMapHom_injective`, `restrictRestrictAlgEquivMapHom_surjective`, `isGalois`, `card_aut_eq_finrank`, `card_aut_eq_finrank`, `card_fixingSubgroup_eq_finrank`, `finiteDimensional_of_finite`, `fixedField_fixingSubgroup`, `fixedField_top`, `fixingSubgroup_normal_of_isGalois`, `integral`, `intermediateFieldEquivSubgroup_apply`, `intermediateFieldEquivSubgroup_symm_apply`, `intermediateFieldEquivSubgroup_symm_apply_toDual`, `is_separable_splitting_field`, `map_fixingSubgroup`, `mem_bot_iff_fixed`, `mem_range_algebraMap_iff_fixed`, `normalAutEquivQuotient_apply`, `normalClosure`, `ofDual_intermediateFieldEquivSubgroup_apply`, `of_algEquiv`, `of_card_aut_eq_finrank`, `of_equiv_equiv`, `of_fixedField_eq_bot`, `of_fixedField_normal_subgroup`, `of_fixed_field`, `of_separable_splitting_field`, `of_separable_splitting_field_aux`, `self`, `separable`, `splits`, `sup_right`, `to_isSeparable`, `to_normal`, `tower_top_intermediateField`, `tower_top_of_isGalois`, `isGalois_bot`, `isGalois_iff`, `isGalois_iff_isGalois_bot`, `isGalois_iff_isGalois_top`	62
Total	75

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`transfer_galois` 📖	mathematical	—	`IsGalois`	—	`IsGalois.of_algEquiv`

Algebra.IsQuadraticExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCyclic` 📖	mathematical	—	`IsCyclic` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `AlgEquiv.aut`	—	`commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `Algebra.instFiniteOfIsQuadraticExtension` `Module.Projective.of_free` `toFree` `AlgEquiv.card_le` `finrank_eq_two` `isCyclic_of_prime_card` `Nat.fact_prime_two` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_le_right` `Nat.card_eq_fintype_card` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `isCyclic_of_subsingleton` `Finite.card_le_one_iff_subsingleton` `Finite.algEquiv` `Finite.algHom` `instIsDomain` `Eq.le`
`isGalois` 📖	mathematical	—	`IsGalois`	—	`commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `normal`
`isMulCommutative_galoisGroup` 📖	mathematical	—	`IsMulCommutative` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut`	—	`commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsCyclic.commutative` `isCyclic`

FixedPoints

Definitions

Name	Category	Theorems
`intermediateField` 📖	CompOp	12 math math: `IsGaloisGroup.fixedPoints_top`, `IsGaloisGroup.fixedPoints_fixingSubgroup`, `IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup`, `IsGaloisGroup.fixingSubgroup_fixedPoints`, `IsGaloisGroup.fixedPoints_bot`, `IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply`, `IsGaloisGroup.subgroup`, `IsGaloisGroup.fixedPoints_le_of_le`, `IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup`, `mem_intermediateField_iff`, `IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual`, `IsGaloisGroup.fixedPoints_eq_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_intermediateField_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `intermediateField` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MulSemiringAction.toDistribMulAction` `Ring.toSemiring`	—	—

IntermediateField

Definitions

Name	Category	Theorems
`fixedField` 📖	CompOp	20 math math: `InfiniteGalois.normalAutEquivQuotient_apply`, `InfiniteGalois.fixingSubgroup_fixedField`, `fixingSubgroup_fixedField`, `mem_fixedField_iff`, `fixedField_antitone`, `InfiniteGalois.fixedField_fixingSubgroup`, `IsGalois.normalAutEquivQuotient_apply`, `IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual`, `InfiniteGalois.restrict_fixedField`, `IsGalois.fixedField_fixingSubgroup`, `IsGalois.intermediateFieldEquivSubgroup_symm_apply`, `IsGalois.fixedField_top`, `finrank_fixedField_eq_card`, `fixedField.isScalarTower`, `fixedField_le`, `le_iff_le`, `InfiniteGalois.fixedField_bot`, `fixedField_bot`, `IsGalois.tfae`, `IsGalois.of_fixedField_normal_subgroup`
`fixingSubgroup` 📖	CompOp	33 math math: `InfiniteGalois.normal_iff_isGalois`, `InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois`, `IsGalois.card_fixingSubgroup_eq_finrank`, `FiniteGaloisIntermediateField.mem_fixingSubgroup_iff`, `InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois`, `InfiniteGalois.fixingSubgroup_fixedField`, `fixingSubgroup_top`, `IsGalois.intermediateFieldEquivSubgroup_apply`, `map_fixingSubgroup`, `fixingSubgroup_fixedField`, `InfiniteGalois.fixedField_fixingSubgroup`, `InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup`, `finrank_eq_fixingSubgroup_index`, `fixingSubgroup_le`, `fixingSubgroup_antitone`, `fixingSubgroup_isClosed`, `IsGalois.fixedField_fixingSubgroup`, `InfiniteGalois.isOpen_iff_finite`, `map_fixingSubgroup_index`, `fixedField.isScalarTower`, `krullTopology_mem_nhds_one_iff`, `krullTopology_mem_nhds_one_iff_of_normal`, `IsGalois.map_fixingSubgroup`, `fixingSubgroup_isOpen`, `le_iff_le`, `IsGalois.fixingSubgroup_normal_of_isGalois`, `restrictNormalHom_ker`, `fixingSubgroup_bot`, `mem_fixingSubgroup_iff`, `InfiniteGalois.fixingSubgroup_isClosed`, `fixingSubgroup_sup`, `IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup`, `IsGalois.ofDual_intermediateFieldEquivSubgroup_apply`
`fixingSubgroupEquiv` 📖	CompOp	—
`restrictRestrictAlgEquivMapHom` 📖	CompOp	3 math math: `restrictRestrictAlgEquivMapHom_apply`, `restrictRestrictAlgEquivMapHom_surjective`, `restrictRestrictAlgEquivMapHom_injective`
`subgroupEquivAlgEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_fixedField_eq_card` 📖	mathematical	—	`Module.finrank` `IntermediateField` `SetLike.instMembership` `instSetLike` `fixedField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instModuleSubtypeMem` `Semiring.toModule` `Nat.card` `AlgEquiv` `Semifield.toCommSemiring` `Subgroup` `AlgEquiv.aut` `Subgroup.instSetLike`	—	`Subgroup.instFiniteSubtypeMem` `Finite.algEquiv` `Finite.algHom` `Module.Free.of_divisionRing` `instIsDomain` `Nat.card_eq_fintype_card` `FixedPoints.finrank_eq_card` `Subgroup.instFaithfulSMulSubtypeMem` `AlgEquiv.apply_faithfulSMul`
`fixedField_antitone` 📖	mathematical	—	`Antitone` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `IntermediateField` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `instPartialOrder` `fixedField`	—	`fixedField_le`
`fixedField_bot` 📖	mathematical	—	`fixedField` `Bot.bot` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instBot` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`ext`
`fixedField_le` 📖	mathematical	`Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder`	`IntermediateField` `instPartialOrder` `fixedField`	—	—
`fixingSubgroup_antitone` 📖	mathematical	—	`Antitone` `IntermediateField` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `PartialOrder.toPreorder` `instPartialOrder` `Subgroup.instPartialOrder` `fixingSubgroup`	—	`fixingSubgroup_le`
`fixingSubgroup_bot` 📖	mathematical	—	`fixingSubgroup` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Top.top` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instTop`	—	`Subgroup.ext` `AlgEquiv.commutes`
`fixingSubgroup_fixedField` 📖	mathematical	—	`fixingSubgroup` `fixedField`	—	`le_iff_le` `le_rfl` `Nat.card_congr` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `Subfield.instSubfieldClass` `Subgroup.instFiniteSubtypeMem` `Finite.algEquiv` `Finite.algHom` `Module.Free.of_divisionRing` `instIsDomain` `Subgroup.instFaithfulSMulSubtypeMem` `AlgEquiv.apply_faithfulSMul` `finiteDimensional_right` `instSubfieldClass` `SetLike.coe_injective` `Set.eq_of_inclusion_surjective` `Nat.bijective_iff_injective_and_card` `Subtype.finite` `Set.inclusion_injective`
`fixingSubgroup_le` 📖	mathematical	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instPartialOrder` `fixingSubgroup`	—	—
`fixingSubgroup_sup` 📖	mathematical	—	`fixingSubgroup` `IntermediateField` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instMin`	—	`Subgroup.ext` `fixingSubgroup_antitone` `le_sup_left` `le_sup_right`
`fixingSubgroup_top` 📖	mathematical	—	`fixingSubgroup` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Bot.bot` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instBot`	—	`Subgroup.ext`
`le_iff_le` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `fixedField` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instPartialOrder` `fixingSubgroup`	—	`Subtype.mem`
`mem_fixedField_iff` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `instSetLike` `fixedField` `DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike`	—	—
`mem_fixingSubgroup_iff` 📖	mathematical	—	`AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `fixingSubgroup` `DFunLike.coe` `AlgEquiv.instFunLike`	—	`mem_fixingSubgroup_iff`
`restrictNormalHom_ker` 📖	mathematical	—	`MonoidHom.ker` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.restrictNormalHom` `instAlgebraSubtypeMem` `isScalarTower_mid'` `fixingSubgroup`	—	`IsScalarTower.left` `isScalarTower_mid'` `AlgEquiv.restrictNormalHom_apply`
`restrictRestrictAlgEquivMapHom_apply` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `instSetLike` `DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `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` `AlgEquiv.instFunLike` `MonoidHom` `instAlgebraSubtypeMem` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `MonoidHom.instFunLike` `restrictRestrictAlgEquivMapHom` `isScalarTower_mid'` `SubsemiringClass.toCommSemiring` `SubringClass.toSubsemiringClass` `DivisionRing.toRing` `Field.toDivisionRing` `SubfieldClass.toSubringClass` `instSubfieldClass`	—	`IsScalarTower.left` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `isScalarTower_mid'` `AlgEquiv.restrictNormalHom_apply`
`restrictRestrictAlgEquivMapHom_injective` 📖	mathematical	`IntermediateField` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`AlgEquiv` `SetLike.instMembership` `instSetLike` `Semifield.toCommSemiring` `Field.toSemifield` `toField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instAlgebraSubtypeMem` `Algebra.id` `algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `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` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `MonoidHom.instFunLike` `restrictRestrictAlgEquivMapHom` `isScalarTower_mid'`	—	`IsScalarTower.left` `isScalarTower_mid'` `injective_iff_map_eq_one` `MonoidHom.instMonoidHomClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `AlgEquiv.apply_smulCommClass'` `Subgroup.mem_bot` `fixingSubgroup_top` `fixingSubgroup_sup` `restrictRestrictAlgEquivMapHom_apply` `AlgEquiv.commutes` `AlgEquiv.ext_iff`
`restrictRestrictAlgEquivMapHom_surjective` 📖	mathematical	`IntermediateField` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `instCompleteLattice` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`AlgEquiv` `SetLike.instMembership` `instSetLike` `Semifield.toCommSemiring` `Field.toSemifield` `toField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instAlgebraSubtypeMem` `Algebra.id` `algebra'` `Algebra.toSMul` `CommSemiring.toSemiring` `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` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `MonoidHom.instFunLike` `restrictRestrictAlgEquivMapHom` `isScalarTower_mid'`	—	`IsScalarTower.left` `isScalarTower_mid'` `eq_bot_iff` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `mem_bot` `IsGalois.mem_bot_iff_fixed` `restrictRestrictAlgEquivMapHom_apply` `mem_fixedField_iff` `mem_inf` `MonoidHom.range_eq_top` `fixingSubgroup_bot` `fixingSubgroup_fixedField`

IntermediateField.fixedField

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	—
`smul` 📖	CompOp	1 math math: `isScalarTower`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isScalarTower` 📖	mathematical	—	`IsScalarTower` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.fixedField` `IntermediateField.fixingSubgroup` `smul` `IntermediateField.instSMulSubtypeMem` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id`	—	`mul_assoc`

IsAlgClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGalois` 📖	mathematical	—	`IsGalois`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsAlgebraic.isSeparable_of_perfectField` `isAlgebraic` `PerfectField.ofCharZero` `normal`

IsGalois

Definitions

Name	Category	Theorems
`galoisCoinsertionIntermediateFieldSubgroup` 📖	CompOp	—
`galoisInsertionIntermediateFieldSubgroup` 📖	CompOp	—
`intermediateFieldEquivSubgroup` 📖	CompOp	4 math math: `intermediateFieldEquivSubgroup_apply`, `intermediateFieldEquivSubgroup_symm_apply_toDual`, `intermediateFieldEquivSubgroup_symm_apply`, `ofDual_intermediateFieldEquivSubgroup_apply`
`normalAutEquivQuotient` 📖	CompOp	1 math math: `normalAutEquivQuotient_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_aut_eq_finrank` 📖	mathematical	—	`Nat.card` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule`	—	`Field.exists_primitive_element` `to_isSeparable` `IsScalarTower.left` `IntermediateField.mem_top` `integral` `separable` `splits` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `AlgEquivClass.toRingEquivClass` `AlgEquiv.instAlgEquivClass` `Polynomial.map_map` `Polynomial.Splits.map` `LinearEquiv.finrank_eq` `IntermediateField.AdjoinSimple.card_aut_eq_finrank` `Nat.card_congr`
`card_fixingSubgroup_eq_finrank` 📖	mathematical	—	`Nat.card` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `SetLike.instMembership` `Subgroup.instSetLike` `IntermediateField.fixingSubgroup` `Module.finrank` `IntermediateField` `IntermediateField.instSetLike` `IntermediateField.toField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IntermediateField.instModuleSubtypeMem` `Semiring.toModule`	—	`fixedField_fixingSubgroup` `IntermediateField.finrank_fixedField_eq_card`
`finiteDimensional_of_finite` 📖	mathematical	—	`FiniteDimensional` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Algebra.toModule` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IsScalarTower.left` `IntermediateField.exists_lt_finrank_of_infinite_dimensional` `Algebra.IsSeparable.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `to_isSeparable` `IntermediateField.isSeparable_tower_bot` `normalClosure.normal` `to_normal` `Nat.card_le_card_of_surjective` `IntermediateField.isScalarTower_mid'` `AlgEquiv.restrictNormalHom_surjective` `LT.lt.not_ge` `LE.le.trans_lt` `card_aut_eq_finrank` `normalClosure.is_finiteDimensional` `IntermediateField.finrank_le_of_le_right` `IntermediateField.le_normalClosure`
`fixedField_fixingSubgroup` 📖	mathematical	—	`IntermediateField.fixedField` `IntermediateField.fixingSubgroup`	—	`IntermediateField.le_iff_le` `le_rfl` `IntermediateField.finrank_fixedField_eq_card` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Nat.card_congr` `card_aut_eq_finrank` `IntermediateField.finiteDimensional_right` `tower_top_intermediateField` `IntermediateField.eq_of_le_of_finrank_eq'`
`fixedField_top` 📖	mathematical	—	`IntermediateField.fixedField` `Top.top` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instTop` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`IntermediateField.fixingSubgroup_bot` `fixedField_fixingSubgroup`
`fixingSubgroup_normal_of_isGalois` 📖	mathematical	—	`Subgroup.Normal` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `IntermediateField.fixingSubgroup`	—	`IsScalarTower.left` `Subgroup.Normal.of_conjugate_fixed` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `map_fixingSubgroup` `IntermediateField.normal_iff_forall_map_eq'` `to_normal`
`integral` 📖	mathematical	—	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Normal.isIntegral` `to_normal`
`intermediateFieldEquivSubgroup_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `IntermediateField` `OrderDual` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `OrderDual.instLE` `Subgroup.instPartialOrder` `RelIso.instFunLike` `intermediateFieldEquivSubgroup` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IntermediateField.fixingSubgroup`	—	—
`intermediateFieldEquivSubgroup_symm_apply` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `IntermediateField` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `IntermediateField.instPartialOrder` `instFunLikeOrderIso` `OrderIso.symm` `intermediateFieldEquivSubgroup` `IntermediateField.fixedField` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`intermediateFieldEquivSubgroup_symm_apply_toDual` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `OrderDual` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `IntermediateField` `OrderDual.instLE` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `IntermediateField.instPartialOrder` `instFunLikeOrderIso` `OrderIso.symm` `intermediateFieldEquivSubgroup` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `IntermediateField.fixedField`	—	—
`is_separable_splitting_field` 📖	mathematical	—	`Polynomial.Separable` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.IsSplittingField`	—	`Field.exists_primitive_element` `to_isSeparable` `separable` `splits` `instIsDomain` `eq_top_iff` `IntermediateField.top_toSubalgebra` `IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic` `IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `integral` `Algebra.adjoin_mono` `Set.singleton_subset_iff` `Polynomial.mem_rootSet` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `minpoly.ne_zero` `minpoly.aeval`
`map_fixingSubgroup` 📖	mathematical	—	`IntermediateField.fixingSubgroup` `IntermediateField.map` `AlgHomClass.toAlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `MulAut` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Subgroup` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAut.instGroup` `MulAction.toSemigroupAction` `Subgroup.pointwiseMulAction` `MulAut.applyMulDistribMulAction` `DFunLike.coe` `MonoidHom` `MonoidHom.instFunLike` `MulAut.conj`	—	`Subgroup.ext` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `Set.image_congr`
`mem_bot_iff_fixed` 📖	mathematical	—	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike`	—	`fixedField_top` `IntermediateField.mem_fixedField_iff`
`mem_range_algebraMap_iff_fixed` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `AlgEquiv` `AlgEquiv.instFunLike`	—	`mem_bot_iff_fixed`
`normalAutEquivQuotient_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `HasQuotient.Quotient` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Subgroup` `AlgEquiv.aut` `QuotientGroup.instHasQuotientSubgroup` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.fixedField` `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` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `normalAutEquivQuotient` `MonoidHom` `MonoidHom.instFunLike` `AlgEquiv.restrictNormalHom` `IntermediateField.instAlgebraSubtypeMem` `IntermediateField.isScalarTower_mid'` `to_normal` `of_fixedField_normal_subgroup`	—	`IsScalarTower.left`
`normalClosure` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.normalClosure` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `Algebra.isSeparable_tower_bot_of_isSeparable` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.isScalarTower_mid'` `to_isSeparable` `normalClosure.normal` `to_normal`
`ofDual_intermediateFieldEquivSubgroup_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `OrderIso` `IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `OrderDual.instLE` `Subgroup.instPartialOrder` `instFunLikeOrderIso` `intermediateFieldEquivSubgroup` `IntermediateField.fixingSubgroup`	—	—
`of_algEquiv` 📖	mathematical	—	`IsGalois`	—	`Algebra.IsSeparable.of_algHom` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `to_isSeparable` `Normal.of_algEquiv` `to_normal`
`of_card_aut_eq_finrank` 📖	mathematical	`Nat.card` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Module.finrank` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule`	`IsGalois`	—	`of_fixedField_eq_bot` `Module.finrank_pos` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.finiteDimensional_right` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `IsScalarTower.left` `IntermediateField.finrank_eq_one_iff` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `Nat.instIsCancelMulZero` `ne_of_lt` `Module.finrank_mul_finrank` `IntermediateField.isScalarTower_mid'` `Module.Free.of_divisionRing` `one_mul` `IntermediateField.finrank_fixedField_eq_card` `Nat.card_congr` `Subgroup.mem_top`
`of_equiv_equiv` 📖	mathematical	`RingHom.comp` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `algebraMap` `RingHomClass.toRingHom` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Distrib.toAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass`	`IsGalois`	—	`RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `isGalois_iff` `Algebra.IsSeparable.of_equiv_equiv` `to_isSeparable` `Normal.of_equiv_equiv` `to_normal`
`of_fixedField_eq_bot` 📖	mathematical	`IntermediateField.fixedField` `Top.top` `Subgroup` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `Subgroup.instTop` `Bot.bot` `IntermediateField` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`IsGalois`	—	`isGalois_iff_isGalois_bot` `of_fixed_field` `Subgroup.instFiniteSubtypeMem` `Finite.algEquiv` `Finite.algHom` `Module.Free.of_divisionRing` `instIsDomain`
`of_fixedField_normal_subgroup` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.fixedField` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `Algebra.isSeparable_tower_bot_of_isSeparable` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IntermediateField.isScalarTower_mid'` `to_isSeparable` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `IntermediateField.normal_iff_forall_map_le'` `to_normal` `AlgEquiv.symm_apply_eq` `Subgroup.Normal.conj_mem'`
`of_fixed_field` 📖	mathematical	—	`IsGalois` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `Subfield.instSetLike` `FixedPoints.subfield` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Subfield.toField` `FixedPoints.instAlgebraSubtypeMemSubfieldSubfield`	—	`FixedPoints.isSeparable` `FixedPoints.normal`
`of_separable_splitting_field` 📖	mathematical	`Polynomial.Separable` `Semifield.toCommSemiring` `Field.toSemifield`	`IsGalois`	—	`instIsDomain` `IntermediateField.toSubalgebra_injective` `IntermediateField.top_toSubalgebra` `top_le_iff` `Polynomial.IsSplittingField.adjoin_rootSet` `IntermediateField.algebra_adjoin_le_adjoin` `IsScalarTower.left` `IntermediateField.induction_on_adjoin_finset` `IntermediateField.card_algHom_adjoin_integral` `isIntegral_zero` `Nat.card_congr` `IntermediateField.adjoin_zero` `IntermediateField.bot_toSubalgebra` `Subalgebra.finrank_bot` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Polynomial.natDegree_X` `minpoly.zero` `IsSeparable.eq_1` `Polynomial.separable_X` `Polynomial.Splits.map` `Polynomial.Splits.X` `IntermediateField.isScalarTower_mid'` `of_separable_splitting_field_aux` `Polynomial.IsSplittingField.finiteDimensional` `Multiset.mem_toFinset` `Module.finrank_mul_finrank` `IntermediateField.instIsScalarTowerSubtypeMem_1` `IsScalarTower.right` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Module.Free.of_divisionRing` `LinearEquiv.finrank_eq` `of_card_aut_eq_finrank`
`of_separable_splitting_field_aux` 📖	mathematical	`Polynomial.Separable` `Semifield.toCommSemiring` `Field.toSemifield` `Multiset` `Multiset.instMembership` `Polynomial.aroots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain`	`Nat.card` `AlgHom` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.restrictScalars` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `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` `Module.toDistribMulAction` `Algebra.toModule` `Module.finrank` `IntermediateField.module'`	—	`instIsDomain` `IsIntegral.tower_top` `isIntegral_of_noetherian` `IsNoetherian.iff_fg` `Multiset.notMem_zero` `Polynomial.aroots_zero` `minpoly.dvd` `Polynomial.aeval_def` `Polynomial.eval₂_map` `Polynomial.eval_map` `IsScalarTower.algebraMap_eq` `Polynomial.mem_roots` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsScalarTower.left` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.isScalarTower` `FiniteDimensional.left` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Nat.card_congr` `Nat.card_sigma` `Finite.of_equiv` `Finite.algHom` `Module.Free.of_divisionRing` `IntermediateField.finiteDimensional_left` `Finite.of_injective` `IntermediateField.adjoin.finrank` `Nat.card_eq_fintype_card` `Finset.sum_const_nat` `IntermediateField.card_algHom_adjoin_integral` `Polynomial.Separable.of_dvd` `Polynomial.separable_map` `Polynomial.Splits.of_dvd` `Polynomial.IsSplittingField.splits` `AlgHom.comp_algebraMap` `Polynomial.map_map` `RingHom.algebraMap_toAlgebra` `Polynomial.map_dvd_map'`
`self` 📖	mathematical	—	`IsGalois` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield`	—	`Algebra.isSeparable_self` `normal_self`
`separable` 📖	mathematical	—	`IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Algebra.IsSeparable.isSeparable` `to_isSeparable`
`splits` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Normal.splits'` `to_normal`
`sup_right` 📖	mathematical	`IntermediateField` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `IntermediateField.instCompleteLattice` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `CompleteLattice.toLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`IsGalois` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring`	—	`IsScalarTower.left` `is_separable_splitting_field` `instIsDomain` `isSplittingField_iff_intermediateField` `Polynomial.map_map` `IsScalarTower.algebraMap_eq` `IntermediateField.isScalarTower_mid'` `Polynomial.Splits.of_algHom` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `SubsemiringClass.nontrivial` `Polynomial.aeval_map_algebraMap` `IntermediateField.restrictScalars_eq_top_iff` `IntermediateField.restrictScalars_adjoin` `IntermediateField.adjoin_union` `IntermediateField.adjoin_self` `Polynomial.Splits.image_rootSet` `IntermediateField.coe_val` `IntermediateField.lift_adjoin` `IntermediateField.lift_top` `sup_comm` `of_separable_splitting_field` `Polynomial.Separable.map`
`to_isSeparable` 📖	mathematical	—	`Algebra.IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	—
`to_normal` 📖	mathematical	—	`Normal`	—	—
`tower_top_intermediateField` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring`	—	`tower_top_of_isGalois` `IsScalarTower.left` `IntermediateField.isScalarTower_mid'`
`tower_top_of_isGalois` 📖	mathematical	—	`IsGalois`	—	`Algebra.isSeparable_tower_top_of_isSeparable` `to_isSeparable` `Normal.tower_top_of_normal` `to_normal`

IsGalois.IntermediateField.AdjoinSimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_aut_eq_finrank` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IsSeparable` `Polynomial.Splits` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IntermediateField.toField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `IntermediateField.algebra'` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `minpoly`	`Nat.card` `AlgEquiv` `Module.finrank` `IntermediateField.module'`	—	`IsScalarTower.left` `IntermediateField.adjoin.finrank` `IntermediateField.card_algHom_adjoin_integral` `Nat.card_congr` `IntermediateField.finiteDimensional_left`

(root)

Definitions

Name	Category	Theorems
`IsGalois` 📖	CompData	35 math math: `InfiniteGalois.normal_iff_isGalois`, `IsGaloisGroup.isGalois`, `IsGalois.tower_top_intermediateField`, `IsGalois.of_algEquiv`, `FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField`, `InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois`, `FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax`, `isGalois_iff_isGalois_top`, `IsGalois.of_fixedField_eq_bot`, `IsAlgClosure.isGalois`, `IsGalois.normalClosure`, `IsGalois.self`, `IsGalois.of_card_aut_eq_finrank`, `IsGalois.sup_right`, `IsGalois.tower_top_of_isGalois`, `IsGalois.of_equiv_equiv`, `FiniteGaloisIntermediateField.isGalois`, `IsCyclotomicExtension.isGalois`, `AlgEquiv.transfer_galois`, `isGalois_iff`, `GaloisField.instIsGaloisOfFinite`, `isGalois_of_isSplittingField_X_pow_sub_C`, `IsSepClosure.isGalois`, `FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin`, `IsGalois.of_fixed_field`, `IsAbelianGalois.toIsGalois`, `IsGalois.tfae`, `Algebra.IsQuadraticExtension.isGalois`, `Ring.instIsGaloisFractionRingNormalClosure`, `isGalois_bot`, `isGalois_iff_isGalois_bot`, `separableClosure.isGalois`, `IsGalois.of_separable_splitting_field`, `IsGalois.of_fixedField_normal_subgroup`, `isCyclic_tfae`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isGalois_bot` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `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` `AlgEquiv.transfer_galois` `IsGalois.self`
`isGalois_iff` 📖	mathematical	—	`IsGalois` `Algebra.IsSeparable` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Normal`	—	`IsGalois.to_isSeparable` `IsGalois.to_normal`
`isGalois_iff_isGalois_bot` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `IntermediateField.toField` `IntermediateField.instAlgebraSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Algebra.id` `Semifield.toCommSemiring`	—	`IsGalois.tower_top_of_isGalois` `IntermediateField.isScalarTower_over_bot` `IsGalois.tower_top_intermediateField`
`isGalois_iff_isGalois_top` 📖	mathematical	—	`IsGalois` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `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`	—	`AlgEquiv.transfer_galois` `IsScalarTower.left`

---

← Back to Index