Documentation Verification Report

IntermediateField

📁 Source: Mathlib/Topology/Algebra/IntermediateField.lean

Statistics

Metric	Count
Definitions `IntermediateField`	1
Theorems `botContinuousSMul`, `continuousSMul`	2
Total	3

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`botContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `IntermediateField` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Algebra.toSMul` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `Field.toCommRing` `SubfieldClass.toSubringClass` `Field.toDivisionRing` `instSubfieldClass` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toField` `algebra'` `algebraOverBot` `instAlgebraSubtypeMem` `Algebra.id` `isScalarTower_over_bot` `instTopologicalSpaceSubtype`	—	`Topology.IsInducing.continuousSMul` `continuousSMul` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `isScalarTower_over_bot` `Topology.IsInducing.subtypeVal` `continuous_id`
`continuousSMul` 📖	mathematical	—	`ContinuousSMul` `IntermediateField` `SetLike.instMembership` `instSetLike` `instSMulSubtypeMem` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MulAction.toSemigroupAction` `instTopologicalSpaceSubtype`	—	`Subfield.continuousSMul`

(root)

Definitions

Name	Category	Theorems
`IntermediateField` 📖	CompData	828 math math: `IsGaloisGroup.smul_mem_of_normal`, `IntermediateField.extendScalars_toSubfield`, `normalClosure_le_iff`, `IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots`, `IntermediateField.finInsepDegree_top`, `Field.Emb.Cardinal.equivLim_coherence`, `InfiniteGalois.normal_iff_isGalois`, `IntermediateField.map_mono`, `IntermediateField.exists_algHom_adjoin_of_splits`, `mem_perfectClosure_iff_natSepDegree_eq_one`, `IntermediateField.aeval_gen_minpoly`, `IntermediateField.adjoin_eq_top_iff_of_isAlgebraic`, `Field.finite_intermediateField_of_exists_primitive_element`, `IntermediateField.LinearDisjoint.iff_inf_eq_bot`, `IntermediateField.normal_inf`, `IntermediateField.algHomEquivAlgHomOfSplits_symm_apply`, `IntermediateField.sSup_toSubfield`, `IsGalois.tower_top_intermediateField`, `IntermediateField.LinearDisjoint.linearIndependent_right'`, `IntermediateField.adjoin.finrank`, `IntermediateField.algebraMap_mem`, `IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic`, `IntermediateField.algHomEquivAlgHomOfSplits_apply_apply`, `IntermediateField.extendScalars_sup`, `IntermediateField.coe_algebraMap_over_bot`, `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`, `IntermediateField.lift_le`, `perfectClosure.map_le_of_algHom`, `RatFunc.algEquivOfTranscendental_X`, `mem_subalgebraEquivIntermediateField`, `minpoly.algEquiv_apply`, `IntermediateField.relrank_comap_comap_eq_relrank_inf`, `IntermediateField.isScalarTower_mid'`, `IntermediateField.map_le_iff_le_comap`, `IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen`, `IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoin`, `IntermediateField.isPurelyInseparable_iSup`, `IntermediateField.coe_prod`, `IntermediateField.coe_bot`, `FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField`, `FiniteGaloisIntermediateField.subset_adjoin`, `Field.Emb.Cardinal.directed_filtration`, `IntermediateField.lift_insepDegree_bot'`, `Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor`, `InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois`, `Field.Emb.Cardinal.filtration_succ`, `IntermediateField.relfinrank_mul_finrank_top`, `IntermediateField.isCyclotomicExtension_le_of_dvd`, `algebraicClosure.algebraicClosure_eq_bot`, `IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right`, `IntermediateField.coe_iSup_of_directed`, `InfiniteGalois.normalAutEquivQuotient_apply`, `IsGaloisGroup.fixingSubgroup_top`, `FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax`, `IntermediateField.isAlgebraic_tower_bot`, `IsGaloisGroup.fixedPoints_top`, `IntermediateField.mem_adjoin_iff`, `IntermediateField.mem_carrier`, `IntermediateField.algHomEquivAlgHomOfSplits_apply`, `IntermediateField.botEquiv_symm`, `IntermediateField.relrank_mul_rank_top`, `IsGalois.card_fixingSubgroup_eq_finrank`, `Subfield.relfinrank_eq_finrank_of_le`, `AlgHom.fieldRange_eq_map`, `IntermediateField.relfinrank_bot_right`, `NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow`, `Field.exists_primitive_element`, `isGalois_iff_isGalois_top`, `IntermediateField.relrank_eq_one_iff`, `RatFunc.IntermediateField.adjoin_X`, `FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1`, `InfiniteGalois.mem_bot_iff_fixed`, `FiniteGaloisIntermediateField.mem_fixingSubgroup_iff`, `IntermediateField.exists_algHom_of_adjoin_splits`, `IntermediateField.normal_iff_forall_map_eq`, `IntermediateField.extendScalars_injective`, `IntermediateField.ext_iff`, `IntermediateField.natCast_mem`, `IntermediateField.adjoin_simple_isCompactElement`, `IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic`, `IntermediateField.coe_neg`, `IntermediateField.adjoin.mono`, `IntermediateField.restrictScalars_normal`, `IntermediateField.isScalarTower`, `IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply`, `Algebra.FormallySmooth.adjoin_of_algebraicIndependent`, `IntermediateField.algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin`, `isPurelyInseparable_iff_fd_isPurelyInseparable`, `IntermediateField.LinearDisjoint.of_isField'`, `IntermediateField.adjoin_zero`, `IntermediateField.coe_iInf`, `PowerBasis.equivAdjoinSimple_symm_aeval`, `IntermediateField.adjoin_univ`, `InfiniteGalois.toAlgEquivAux_eq_proj_of_mem`, `Subfield.coe_toIntermediateField`, `IntermediateField.lift_adjoin_simple`, `algebraicClosure.normalClosure_eq_self`, `IntermediateField.AdjoinDouble.normal_algebraicClosure`, `IntermediateField.coe_add`, `IntermediateField.mem_adjoin_simple_self`, `IntermediateField.prod_mem`, `IntermediateField.isAlgebraic_adjoin_iff_top`, `IntermediateField.inf_toSubalgebra`, `algebraicClosure.isAlgebraic`, `IntermediateField.adjoin_finite_isCompactElement`, `IsGalois.normalClosure`, `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow'`, `IntermediateField.finiteDimensional_right`, `IntermediateField.isAlgebraic_iff`, `RatFunc.Luroth.algEquiv_apply`, `IntermediateField.charZero`, `NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic`, `IntermediateField.mem_adjoin_of_mem`, `IntermediateField.subset_adjoin_of_subset_left`, `IntermediateField.instSMulMemClass`, `IntermediateField.coe_inclusion`, `IntermediateField.adjoin_le_iff`, `IntermediateField.finiteDimensional_iSup_of_finset`, `NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex`, `IntermediateField.LinearDisjoint.of_le`, `IsGaloisGroup.quotientMap`, `IsNormalClosure.adjoin_rootSet`, `IntermediateField.LinearDisjoint.trace_algebraMap`, `instIsAbelianGaloisSubtypeMemIntermediateFieldBot`, `Field.Emb.Cardinal.two_le_deg`, `IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic`, `IntermediateField.div_mem`, `IntermediateField.smulCommClass_left`, `IntermediateField.finInsepDegree_le_of_left_le`, `IntermediateField.isAlgebraic_adjoin_iff`, `IntermediateField.minpoly_gen`, `Field.Emb.Cardinal.isLeast_leastExt`, `IntermediateField.aeval_coe`, `IntermediateField.instIsScalarTowerSubtypeMem`, `RatFunc.IntermediateField.isAlgebraic_X`, `IsKrasner.krasner'`, `IntermediateField.inf_relrank_right`, `normalClosure_eq_iSup_adjoin'`, `IntermediateField.iInf_toSubfield`, `IntermediateField.fixingSubgroup_top`, `IntermediateField.coe_toSubalgebra`, `Field.Emb.Cardinal.succEquiv_coherence`, `IntermediateField.bot_toSubalgebra`, `IntermediateField.isScalarTower_bot`, `IntermediateField.sup_toSubalgebra_of_isAlgebraic_left`, `IntermediateField.relfinrank_top_right`, `IntermediateField.restrictScalars_sup`, `FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin`, `IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff`, `IntermediateField.linearDisjoint_comm`, `IsGaloisGroup.of_fixedPoints_eq`, `IntermediateField.Lifts.exists_lift_of_splits'`, `Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `IntermediateField.restrictScalars_top`, `IntermediateField.equivOfEq_symm`, `IntermediateField.coe_type_toSubfield`, `IntermediateField.restrictRestrictAlgEquivMapHom_apply`, `IsGalois.intermediateFieldEquivSubgroup_apply`, `IntermediateField.mem_top`, `IntermediateField.fieldRange_comp_val`, `Subfield.extendScalars_le_extendScalars_iff`, `Field.primitive_element_iff_algHom_eq_of_eval'`, `IntermediateField.adjoin.powerBasis_gen`, `IntermediateField.equivOfEq_rfl`, `IntermediateField.normal_iff_normalClosure_le`, `mem_perfectClosure_iff_pow_mem`, `Subfield.extendScalars_inf`, `IntermediateField.relrank_top_right`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1`, `IntermediateField.LinearDisjoint.bot_left`, `IntermediateField.isTotallyReal_bot`, `IntermediateField.continuousSMul`, `IsGaloisGroup.quotient`, `IntermediateField.relfinrank_dvd_finrank_bot`, `IsGalois.sup_right`, `IntermediateField.exists_finset_maximalFor_isTranscendenceBasis_separableClosure`, `IntermediateField.adjoin_simple_adjoin_simple`, `normalClosure.restrictScalars_eq`, `IntermediateField.normal_iSup`, `IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right`, `IntermediateField.mem_adjoin_pair_right`, `IntermediateField.restrictRestrictAlgEquivMapHom_surjective`, `IsGaloisGroup.instSMulCommClassQuotientSubgroupSubtypeMemIntermediateField`, `IntermediateField.multiset_prod_mem`, `IntermediateField.AdjoinSimple.norm_gen_eq_one`, `IntermediateField.range_val`, `IntermediateField.instFiniteSubtypeMemBot`, `IntermediateField.isCyclotomicExtension_lcm_sup`, `IntermediateField.LinearDisjoint.linearIndependent_mul`, `map_mem_perfectClosure_iff`, `IntermediateField.sup_toSubalgebra_of_isAlgebraic`, `IntermediateField.linearDisjoint_iff'`, `IsGaloisGroup.fixedPoints_fixingSubgroup`, `IntermediateField.splits_iff_mem`, `IntermediateField.extendScalars.orderIso_apply`, `IntermediateField.LinearDisjoint.basisOfBasisLeft_apply`, `algebraicClosure.isIntegralClosure`, `Algebra.normalizedTrace_intermediateField`, `IntermediateField.add_mem`, `IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup`, `isNormalClosure_normalClosure`, `IntermediateField.mem_fixedField_iff`, `IntermediateField.finrank_eq_one_iff`, `IntermediateField.lift_top`, `solvableByRad_le`, `IsGaloisGroup.fixingSubgroup_le_of_le`, `RatFunc.adjoin_X`, `IntermediateField.sInf_toSubalgebra`, `Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet`, `IntermediateField.finrank_lt_of_gt`, `IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic`, `map_mem_separableClosure_iff`, `IntermediateField.insepDegree_bot'`, `IntermediateField.fixedField_antitone`, `IntermediateField.exists_algHom_adjoin_of_splits_of_aeval`, `IntermediateField.LinearDisjoint.basisOfBasisRight_apply`, `AlgebraicIndependent.lift_reprField`, `IntermediateField.isAlgebraic_adjoin`, `IntermediateField.fg_sup`, `IntermediateField.inf_relfinrank_right`, `mem_subalgebraEquivIntermediateField_symm`, `instIsLiouvilleSubtypeMemIntermediateField`, `IntermediateField.coe_mul`, `IntermediateField.sSup_def`, `IntermediateField.restrictScalars_eq_top_iff`, `IsTranscendenceBasis.isAlgebraic_field`, `RatFunc.Luroth.algEquiv_algebraMap`, `NumberField.hermiteTheorem.finite_of_finite_generating_set`, `Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `PowerBasis.equivAdjoinSimple_aeval`, `IntermediateField.extendScalars_adjoin`, `IntermediateField.isPurelyInseparable_tower_bot`, `IntermediateField.neg_mem`, `le_separableClosure_iff`, `IntermediateField.charP'`, `IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one`, `RatFunc.algEquivOfTranscendental_symm_gen`, `toIntermediateField'_toSubalgebra`, `RatFunc.Luroth.generator_mem`, `IntermediateField.extendScalars_inf`, `IntermediateField.botContinuousSMul`, `IntermediateField.LinearDisjoint.of_le_right`, `separableClosure_le`, `Field.exists_primitive_element_of_finite_bot`, `IntermediateField.restrictScalars_le_iff`, `eq_separableClosure_iff`, `separableClosure.map_le_of_algHom`, `IntermediateField.mem_toSubfield`, `mem_algebraicClosure_iff`, `IntermediateField.normal_iff_forall_fieldRange_le`, `IsGalois.normalAutEquivQuotient_apply`, `Field.exists_primitive_element_of_finite_top`, `IntermediateField.instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap`, `IntermediateField.adjoin_simple_eq_top_iff_of_isAlgebraic`, `IntermediateField.LinearDisjoint.finrank_right_eq_finrank`, `NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex`, `IntermediateField.instSubfieldClass`, `trace_eq_finrank_mul_minpoly_nextCoeff`, `IntermediateField.rank_adjoin_eq_one_iff`, `normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1`, `IntermediateField.isAlgebraic_tower_top`, `IntermediateField.adjoin_one`, `IntermediateField.rank_top`, `IntermediateField.finrank_eq_fixingSubgroup_index`, `trace_eq_trace_adjoin`, `IntermediateField.coe_isIntegral_iff`, `IntermediateField.adjoin_root_eq_top`, `Submodule.traceDual_le_span_map_traceDual`, `IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right`, `IsGaloisGroup.fixingSubgroup_fixedPoints`, `InfiniteGalois.proj_adjoin_singleton_val`, `normalClosure_def`, `IntermediateField.lift_inf`, `IntermediateField.instIsCompactlyGenerated`, `IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank`, `mem_perfectClosure_iff`, `IntermediateField.smul_mem`, `IntermediateField.exists_finset_of_mem_supr''`, `IntermediateField.exists_algHom_of_splits`, `IntermediateField.extendScalars_self`, `FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1`, `PowerBasis.equivAdjoinSimple_gen`, `Subfield.extendScalars.orderIso_symm_apply`, `IntermediateField.coe_inf`, `Field.Emb.Cardinal.equivSucc_coherence`, `IntermediateField.finrank_top`, `IntermediateField.restrictScalars_adjoin_eq_sup`, `FiniteGaloisIntermediateField.isGalois`, `separableClosure.eq_top_iff`, `IntermediateField.mem_adjoin_iff_div`, `le_algebraicClosure`, `IntermediateField.LinearDisjoint.finrank_left_eq_finrank`, `IntermediateField.Lifts.lt_iff`, `IntermediateField.mem_inf`, `IntermediateField.top_toSubalgebra`, `IntermediateField.extendScalars_le_iff`, `instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `IntermediateField.cardinalMk_adjoin_le`, `IntermediateField.coe_sum`, `IntermediateField.relrank_top_left`, `IsGaloisGroup.fixedPoints_bot`, `IntermediateField.restrictScalars_injective`, `Splits.algebraicClosure`, `PowerBasis.equivAdjoinSimple_symm_gen`, `IntermediateField.coe_val`, `exists_root_adjoin_eq_top_of_isCyclic`, `RatFunc.finrank_eq_max_natDegree`, `IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply`, `IntermediateField.finrank_eq_finrank_subalgebra`, `IntermediateField.finrank_eq_one_iff_eq_top`, `IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable'`, `IntermediateField.restrictRestrictAlgEquivMapHom_injective`, `IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual`, `IntermediateField.list_sum_mem`, `Subfield.extendScalars_top`, `Transcendental.algebraicClosure`, `IntermediateField.coe_toSubfield`, `IntermediateField.LinearDisjoint.finrank_sup`, `NumberField.is_primitive_element_of_infinitePlace_lt`, `IntermediateField.finrank_adjoin_eq_one_iff`, `Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `algebraicClosure.map_le_of_algHom`, `IntermediateField.normal_iff_forall_map_le'`, `IntermediateField.subsingleton_of_rank_adjoin_eq_one`, `IntermediateField.bot_eq_top_of_rank_adjoin_eq_one`, `IntermediateField.normal_iff_forall_fieldRange_eq`, `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType`, `instIsAbelianGaloisSubtypeMemIntermediateField_1`, `IntermediateField.restrictScalars_inf`, `IntermediateField.instFaithfulSMulSubtypeMem`, `IntermediateField.finrank_bot`, `IntermediateField.fixingSubgroup_antitone`, `InfiniteGalois.restrict_fixedField`, `instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois`, `IntermediateField.subset_adjoin_of_subset_right`, `algebraicClosure.le_restrictScalars`, `IntermediateField.sepDegree_bot`, `normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure`, `trace_eq_sum_roots`, `IntermediateField.algebraMap_apply`, `IntermediateField.exists_finset_of_mem_iSup`, `IntermediateField.adjoin_simple_le_iff`, `IntermediateField.finInsepDegree_bot'`, `RatFunc.minpolyX_aeval_X`, `RatFunc.algEquivOfTranscendental_symm_aeval`, `Algebra.norm_eq_norm_adjoin`, `IntermediateField.subset_adjoin`, `IntermediateField.isAlgebraic_adjoin_iff_isAlgebraic`, `IntermediateField.LinearDisjoint.norm_algebraMap`, `IntermediateField.restrictScalars_bot_eq_self`, `IntermediateField.adjoin.range_algebraMap_subset`, `IntermediateField.fg_bot`, `IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable`, `IntermediateField.sup_def`, `IntermediateField.mem_lift`, `IntermediateField.isAlgebraic_adjoin_pair`, `IntermediateField.finrank_sup_le`, `le_perfectClosure`, `Differential.instDifferentialAlgebraSubtypeMemIntermediateField_1`, `IntermediateField.adjoin_empty`, `IntermediateField.list_prod_mem`, `IntermediateField.adjoinRootEquivAdjoin_apply_root`, `IntermediateField.normalClosureOperator_apply`, `Field.Emb.Cardinal.eq_bot_of_not_nonempty`, `IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree`, `IntermediateField.rank_bot`, `separableClosure_inf_perfectClosure`, `IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem`, `le_restrictScalars_separableClosure`, `IntermediateField.coe_zero`, `separableClosure.adjoin_eq_of_isAlgebraic`, `IntermediateField.adjoin.algebraMap_mem`, `IntermediateField.coe_restrictScalars`, `IntermediateField.instIsScalarTowerSubtypeMem_1`, `IntermediateField.normal`, `IntermediateField.finrank_bot_mul_relfinrank`, `RatFunc.irreducible_minpolyX`, `IsIntegral.mem_intermediateField_of_minpoly_splits`, `IntermediateField.map_injective`, `IntermediateField.LinearDisjoint.of_basis_right`, `IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right`, `IntermediateField.bot_eq_top_iff_finrank_eq_one`, `IntermediateField.finiteDimensional_adjoin`, `IntermediateField.isTranscendenceBasis_adjoin_iff`, `IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left`, `IntermediateField.lift_injective`, `IntermediateField.adjoin_eq_bot_iff`, `RatFunc.Luroth.algEquiv_X`, `IntermediateField.coe_extendScalars`, `IntermediateField.isSeparable_adjoin_simple_iff_isSeparable`, `IntermediateField.AdjoinSimple.trace_gen_eq_zero`, `IntermediateField.lift_sepDegree_bot'`, `IntermediateField.mem_adjoin_range_iff`, `IntermediateField.relfinrank_inf_mul_relfinrank`, `IntermediateField.relrank_dvd_rank_top_of_le`, `RatFunc.natDegree_minpolyX`, `IntermediateField.algebraAdjoinAdjoin.algebraMap_eq_gen_self`, `IntermediateField.finSepDegree_adjoin_simple_le_finrank`, `IntermediateField.LinearDisjoint.inf_eq_bot`, `Field.exists_primitive_element_iff_finite_intermediateField`, `IntermediateField.card_algHom_adjoin_integral`, `Field.Emb.Cardinal.filtration_apply`, `IntermediateField.gc_map_comap`, `IntermediateField.relrank_dvd_rank_bot`, `IntermediateField.AdjoinPair.algebraMap_gen₁`, `Subfield.le_extendScalars_iff`, `IntermediateField.map_comap_eq`, `IsGalois.intermediateFieldEquivSubgroup_symm_apply`, `IntermediateField.sub_mem`, `IntermediateField.map_iSup`, `NumberField.finite_of_discr_bdd`, `IntermediateField.map_iInf`, `IntermediateField.LinearDisjoint.of_inf_eq_bot`, `AlgHom.coe_fieldRange`, `AlgebraicIndependent.liftAlgHom_comp_reprField`, `IntermediateField.finrank_top'`, `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top`, `IntermediateField.inclusion_self`, `IntermediateField.lift_bot`, `NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal`, `IsGalois.fixedField_top`, `IntermediateField.normalClosure_of_normal`, `IntermediateField.charP`, `Algebra.IsAlgebraic.isNormalClosure_iff`, `IntermediateField.intCast_mem`, `RatFunc.minpolyX_eq_zero_iff`, `IntermediateField.sup_toSubalgebra_of_left`, `InfiniteGalois.isOpen_iff_finite`, `IntermediateField.isSplittingField_iSup`, `Field.Emb.Cardinal.deg_lt_aleph0`, `IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen`, `IntermediateField.adjoin_simple_eq_bot_iff`, `IntermediateField.relfinrank_bot_left`, `solvableByRad.rad_mem`, `IntermediateField.toSubalgebra_injective`, `IntermediateField.iSup_eq_adjoin`, `IntermediateField.LinearDisjoint.rank_sup`, `IntermediateField.le_extendScalars_iff`, `Subfield.extendScalars_le_iff`, `IntermediateField.rank_sup_le_of_isAlgebraic`, `IntermediateField.extendScalars.orderIso_symm_apply_coe`, `exists_isTranscendenceBasis_and_isSeparable_of_perfectField`, `solvableByRad_le_algClosure`, `IntermediateField.adjoin_intCast`, `IntermediateField.iSup_toSubfield`, `IntermediateField.sepDegree_bot'`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `IntermediateField.inclusion_injective`, `Differential.instDifferentialAlgebraSubtypeMemIntermediateField`, `IsGaloisGroup.subgroup_iff`, `IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left`, `IntermediateField.LinearDisjoint.bot_right`, `Field.primitive_element_iff_minpoly_degree_eq`, `AlgHom.fieldRange_eq_top`, `IntermediateField.normal_iff_forall_map_le`, `separableClosure.isAlgebraic`, `IntermediateField.normalClosureOperator_isClosed`, `Subfield.extendScalars.orderIso_apply`, `IntermediateField.expChar`, `isPurelyInseparable_iff_perfectClosure_eq_top`, `IntermediateField.rank_eq_one_iff`, `IsGaloisGroup.intermediateField`, `IntermediateField.relfinrank_mul_relfinrank_eq_inf_relfinrank`, `IntermediateField.adjoin_rank_le_of_isAlgebraic_right`, `IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_left`, `IntermediateField.fg_iSup`, `IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable`, `spectralNorm.eq_of_normalClosure`, `IntermediateField.LinearDisjoint.linearIndependent_right`, `IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply`, `NumberField.linearDisjoint_of_isGalois_isCoprime_discr`, `IntermediateField.mem_adjoin_pair_left`, `Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin`, `IntermediateField.adjoin_root_eq_top_of_isSplittingField`, `spectralNorm.eq_of_normalClosure'`, `algebraicClosure.eq_top_iff`, `IntermediateField.adjoin_iUnion`, `algebraicClosure.adjoin_le`, `AlgHom.mem_fieldRange`, `IntermediateField.finrank_fixedField_eq_card`, `separableClosure.isSepClosure`, `IntermediateField.finrank_comap`, `InfiniteGalois.toAlgEquivAux_eq_liftNormal`, `Field.primitive_element_iff_minpoly_natDegree_eq`, `IntermediateField.normalClosure_def''`, `Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint`, `IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots`, `Subfield.relrank_eq_rank_of_le`, `Field.Emb.Cardinal.strictMono_filtration`, `IntermediateField.relfinrank_eq_finrank_of_le`, `FixedBy.intermediateField_mem_iff`, `IntermediateField.isScalarTower_over_bot`, `IntermediateField.isSeparable_tower_bot`, `IntermediateField.minpoly_eq`, `IntermediateField.exists_finset_of_mem_adjoin`, `IntermediateField.relfinrank_inf_mul_relfinrank_of_le`, `IsGaloisGroup.coe_quotient_smul`, `IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left`, `IntermediateField.mem_toSubalgebra`, `IntermediateField.isSplittingField_iff`, `IntermediateField.bot_toSubfield`, `IntermediateField.topEquiv_symm_apply_coe`, `FiniteGaloisIntermediateField.adjoin_val`, `IntermediateField.adjoin_finset_isCompactElement`, `NumberField.of_intermediateField`, `IntermediateField.adjoin_eq_range_algebraMap_adjoin`, `IntermediateField.relrank_inf_mul_relrank_of_le`, `IntermediateField.multiset_sum_mem`, `IntermediateField.rank_top'`, `IntermediateField.isAlgebraic_adjoin_simple`, `IntermediateField.exists_finset_of_mem_supr'`, `IntermediateField.AdjoinSimple.normal_algebraicClosure`, `IntermediateField.normal_iff_forall_map_eq'`, `IntermediateField.intermediateFieldMap_apply_coe`, `IntermediateField.topEquiv_apply`, `IntermediateField.LinearDisjoint.symm`, `IntermediateField.exists_algHom_adjoin_of_splits'`, `Algebra.normalizedTrace_def`, `IntermediateField.adjoin_natCast`, `IntermediateField.coe_inv`, `IntermediateField.AdjoinSimple.isIntegral_gen`, `RatFunc.natDegree_num_le_natDegree_minpolyX`, `map_mem_algebraicClosure_iff`, `IntermediateField.mem_restrictScalars`, `IntermediateField.mem_sInf`, `IntermediateField.exists_lt_finrank_of_infinite_dimensional`, `IntermediateField.adjoin_rank_le_of_isAlgebraic`, `IntermediateField.normal_iInf`, `Algebra.IsAlgebraic.isNormalClosure_normalClosure`, `IntermediateField.mul_mem`, `IntermediateField.isPurelyInseparable_bot`, `mem_algebraicClosure_iff'`, `IntermediateField.top_toSubfield`, `AlgebraicIndependent.aevalEquivField_apply_coe`, `IntermediateField.LinearDisjoint.exists_field_of_isDomain`, `IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_right`, `Subfield.extendScalars_sup`, `IntermediateField.isSeparable_adjoin_pair_of_isSeparable`, `IntermediateField.finiteDimensional_left`, `IntermediateField.finiteDimensional_iSup_of_finite`, `le_perfectClosure_iff`, `perfectClosure.isAlgebraic`, `IntermediateField.isSeparable_sup`, `FiniteGaloisIntermediateField.finiteDimensional`, `IntermediateField.map_mem_map`, `IsGaloisGroup.smul_eq_self`, `AlgHom.fieldRange_le_normalClosure`, `RatFunc.Luroth.adjoin_generator_le`, `IntermediateField.smul_def`, `InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj`, `IntermediateField.coe_smul`, `IsGaloisGroup.fixingSubgroup_bot`, `Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `IntermediateField.relfinrank_dvd_finrank_top_of_le`, `IntermediateField.set_range_subset`, `InfiniteGalois.restrictNormalHom_continuous`, `IntermediateField.isAlgebraic_iSup`, `IntermediateField.subsingleton_of_finrank_adjoin_eq_one`, `IsGaloisGroup.subgroup`, `normalClosure_eq_iSup_adjoin`, `IntermediateField.LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left`, `IntermediateField.fixedField.isScalarTower`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `IsGalois.of_separable_splitting_field_aux`, `IntermediateField.coe_equivMap_apply`, `IntermediateField.fg_top`, `IntermediateField.adjoin_insert_adjoin`, `IntermediateField.mem_adjoin_simple_iff`, `IntermediateField.finrank_le_of_le_left`, `IntermediateField.finInsepDegree_bot`, `IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic`, `IsGaloisGroup.intermediateFieldEquivSubgroup_apply`, `krullTopology_mem_nhds_one_iff`, `IntermediateField.one_mem`, `AlgEquiv.fieldRange_eq_top`, `IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot`, `IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin`, `Field.Emb.Cardinal.iSup_adjoin_eq_top`, `IntermediateField.toSubalgebra_iSup_of_directed`, `IntermediateField.lift_cardinalMk_adjoin_le`, `IntermediateField.isSeparable_iSup`, `krullTopology_mem_nhds_one_iff_of_normal`, `IntermediateField.finrank_bot'`, `IntermediateField.sInf_toSubfield`, `IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot`, `IntermediateField.Lifts.exists_lift_of_splits`, `separableClosure.isSeparable`, `RatFunc.isAlgebraic_adjoin_simple_X'`, `IntermediateField.adjoin_toSubalgebra_of_isAlgebraic_left`, `Algebra.norm_eq_prod_roots`, `IntermediateField.adjoin.finiteDimensional`, `IntermediateField.botEquiv_def`, `le_algebraicClosure_iff`, `IntermediateField.adjoin_adjoin_comm`, `IntermediateField.adjoin_eq_top_iff`, `AlgebraicIndependent.algebraicClosure`, `IntermediateField.toSubalgebra_lt_toSubalgebra`, `IntermediateField.finSepDegree_bot'`, `IntermediateField.val_mk`, `IntermediateField.rank_sup_le`, `IntermediateField.coe_pow`, `IntermediateField.fixedField_le`, `IntermediateField.eq_bot_of_isSepClosed_of_isSeparable`, `FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField`, `AlgEquiv.restrictNormalHom_apply`, `InfiniteGalois.mk_toAlgEquivAux`, `instIsAbelianGaloisSubtypeMemIntermediateField`, `IntermediateField.adjoin_simple_comm`, `algebraicClosure.isAlgClosure`, `IntermediateField.pow_mem`, `IntermediateField.inclusion_inclusion`, `IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic`, `IntermediateField.bot_eq_top_of_finrank_adjoin_le_one`, `IntermediateField.relrank_bot_right`, `IntermediateField.le_iff_le`, `IntermediateField.extendScalars_restrictScalars`, `InfiniteGalois.fixedField_bot`, `IntermediateField.zero_mem`, `IntermediateField.adjoin_subset_adjoin_iff`, `IsSepClosed.separableClosure_eq_bot_iff`, `IntermediateField.mem_extendScalars`, `perfectClosure.perfectField`, `FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin`, `Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet`, `IntermediateField.mem_mk`, `RatFunc.C_minpolyX`, `InfiniteGalois.proj_of_le`, `IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf`, `IntermediateField.expChar'`, `exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow`, `IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element`, `IntermediateField.adjoin_eq_top_of_adjoin_eq_top`, `IntermediateField.coe_type_toSubalgebra`, `IntermediateField.relrank_eq_rank_of_le`, `IntermediateField.adjoin_union`, `IntermediateField.inf_toSubfield`, `IntermediateField.lift_adjoin`, `IntermediateField.coe_copy`, `FiniteGaloisIntermediateField.val_injective`, `IntermediateField.smulCommClass_right`, `IntermediateField.adjoin_eq_top_of_algebra`, `IsGaloisGroup.fixedPoints_le_of_le`, `IntermediateField.extendScalars_top`, `perfectClosure.eq_bot_of_isSeparable`, `IntermediateField.algebraicIndependent_adjoin_iff`, `mem_separableClosure_iff`, `IntermediateField.rank_eq_rank_subalgebra`, `le_separableClosure'`, `IntermediateField.fixedField_bot`, `IntermediateField.LinearDisjoint.of_finrank_sup`, `AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe`, `IntermediateField.toSubalgebra_strictMono`, `IntermediateField.lift_sup`, `normalClosure.normal`, `IntermediateField.adjoin_adjoin_left`, `IntermediateField.normalClosure_mono`, `IntermediateField.AdjoinSimple.coe_aeval_gen_apply`, `IntermediateField.LinearDisjoint.linearIndependent_mul'`, `separableClosure_le_iff`, `IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply`, `IntermediateField.restrictNormalHom_ker`, `FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin`, `IntermediateField.adjoin_rank_le_of_isAlgebraic_left`, `isClosed_restrictScalars_separableClosure`, `IntermediateField.sup_toSubalgebra_of_right`, `IntermediateField.algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin`, `IntermediateField.insepDegree_bot`, `IsAlgClosed.algebraicClosure_eq_bot_iff`, `IntermediateField.equivOfEq_apply`, `IntermediateField.rank_bot'`, `IntermediateField.le_sup_toSubalgebra`, `IntermediateField.gc`, `IntermediateField.isAlgebraic_adjoin_iff_bot`, `FiniteGaloisIntermediateField.le_iff`, `IntermediateField.fieldRange_val`, `IntermediateField.liftAlgEquiv_apply`, `IntermediateField.LinearDisjoint.of_basis_mul`, `IntermediateField.inv_mem`, `IntermediateField.insepDegree_top`, `separableClosure_le_separableClosure_iff`, `IsGalois.tfae`, `IntermediateField.map_inf`, `IntermediateField.transcendental_adjoin_iff`, `Field.Emb.Cardinal.iSup_filtration`, `IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1`, `IntermediateField.isSimpleOrder_of_finrank_prime`, `IntermediateField.LinearDisjoint.eq_bot_of_self`, `IntermediateField.rank_comap`, `separableClosure.separableClosure_eq_bot`, `IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right`, `le_separableClosure`, `IntermediateField.rank_bot_mul_relrank`, `IntermediateField.fg_top_iff`, `IntermediateField.sup_toSubfield`, `IntermediateField.relfinrank_comap_comap_eq_relfinrank_inf`, `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right`, `IntermediateField.toSubalgebra_le_toSubalgebra`, `instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois`, `IntermediateField.inf_relfinrank_left`, `IntermediateField.relfinrank_top_left`, `IntermediateField.map_sup`, `IntermediateField.subsingleton_of_finrank_adjoin_le_one`, `IntermediateField.finiteDimensional_map`, `RatFunc.algEquivOfTranscendental_algebraMap`, `IntermediateField.finSepDegree_top`, `IntermediateField.lift_rank_comap`, `IntermediateField.inf_relrank_left`, `IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_right`, `IsAdjoinRoot.primitive_element_root`, `IntermediateField.instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap`, `IntermediateField.normalClosure_le_iff_of_normal`, `AlgHom.fieldRange_of_normal`, `IntermediateField.Lifts.eq_iff`, `Subfield.extendScalars_self`, `Field.Emb.Cardinal.adjoin_basis_eq_top`, `IntermediateField.relrank_inf_mul_relrank`, `IntermediateField.iInf_toSubalgebra`, `IsGaloisGroup.card_fixingSubgroup_eq_finrank`, `IntermediateField.normalClosure_map_eq`, `IntermediateField.LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left`, `IntermediateField.relrank_bot_left`, `IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension`, `IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup`, `Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `Subfield.mem_extendScalars`, `RatFunc.isAlgebraic_adjoin_simple_X`, `IntermediateField.isPurelyInseparable_tower_top`, `IntermediateField.le_normalClosure`, `IntermediateField.equivOfEq_trans`, `IntermediateField.Lifts.carrier_union`, `IntermediateField.mem_map`, `IntermediateField.toSubfield_injective`, `IntermediateField.normalClosure_def'`, `IntermediateField.adjoin_self`, `IntermediateField.mem_bot`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1`, `IntermediateField.mem_restrict`, `perfectClosure.perfectRing`, `FixedPoints.mem_intermediateField_iff`, `IntermediateField.LinearDisjoint.isDomain`, `IntermediateField.finrank_dvd_of_le_right`, `IntermediateField.relrank_mul_relrank_eq_inf_relrank`, `IntermediateField.fixingSubgroup_bot`, `IntermediateField.finrank_le_of_le_right`, `RatFunc.natDegree_denom_le_natDegree_minpolyX`, `IntermediateField.coe_top`, `IntermediateField.AdjoinSimple.coe_gen`, `isGalois_bot`, `IntermediateField.intermediateFieldMap_symm_apply_coe`, `IntermediateField.finrank_dvd_of_le_left`, `IntermediateField.coe_sInf`, `isSplittingField_iff_intermediateField`, `IntermediateField.FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure`, `isGalois_iff_isGalois_bot`, `Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits`, `IntermediateField.LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic`, `Field.insepDegree_le_of_left_le`, `IntermediateField.finiteDimensional_adjoin_pair`, `IsKrasner.krasner`, `IntermediateField.normal_sup`, `IntermediateField.coe_algebraMap_apply`, `separableClosure.isGalois`, `IntermediateField.isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one`, `IntermediateField.coe_div`, `IntermediateField.restrictScalars_adjoin`, `IntermediateField.finiteDimensional_iSup_of_finset'`, `IntermediateField.finrank_adjoin_simple_eq_one_iff`, `IntermediateField.zsmul_mem`, `IntermediateField.LinearDisjoint.map`, `IntermediateField.isSeparable_tower_top`, `RatFunc.algEquivOfTranscendental_apply`, `normalClosure.is_finiteDimensional`, `Field.primitive_element_iff_algHom_eq_of_eval`, `IntermediateField.finiteDimensional_sup`, `IntermediateField.Lifts.le_iff`, `Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin`, `separableClosure.eq_bot_iff`, `trace_adjoinSimpleGen`, `IntermediateField.fixingSubgroup_sup`, `IntermediateField.normal_iff_normalClosure_eq`, `IntermediateField.rank_adjoin_simple_eq_one_iff`, `IntermediateField.algebraAdjoinAdjoin.coe_algebraMap`, `separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable`, `IntermediateField.AdjoinPair.algebraMap_gen₂`, `IntermediateField.isIntegral_iff`, `IntermediateField.LinearDisjoint.isField_of_isAlgebraic`, `Subfield.coe_extendScalars`, `separableClosure.normalClosure_eq_self`, `IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup`, `IntermediateField.coe_map`, `Subfield.extendScalars_injective`, `IntermediateField.adjoin.powerBasis_dim`, `IsGalois.of_fixedField_normal_subgroup`, `IntermediateField.relfinrank_eq_one_iff`, `IntermediateField.essFiniteType_iff`, `Field.Emb.cardinal_separableClosure`, `IntermediateField.AdjoinSimple.algebraMap_gen`, `IntermediateField.isPurelyInseparable_sup`, `IntermediateField.splits_of_splits`, `IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual`, `separableClosure.adjoin_le`, `IsGalois.mem_bot_iff_fixed`, `FiniteGaloisIntermediateField.adjoin_simple_le_iff`, `separableClosure.le_restrictScalars`, `IntermediateField.map_bot`, `le_algebraicClosure'`, `IntermediateField.sum_mem`, `separableClosure.isPurelyInseparable`, `IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem`, `isCyclic_tfae`, `separableClosure.eq_bot_of_isPurelyInseparable`, `IntermediateField.adjoin_rootSet_isSplittingField`, `IntermediateField.nonempty_algHom_adjoin_of_splits`, `IntermediateField.isScalarTower_mid`, `IntermediateField.finSepDegree_bot`, `IntermediateField.biSup_adjoin_simple`, `IsGalois.ofDual_intermediateFieldEquivSubgroup_apply`, `IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed`, `IntermediateField.LinearDisjoint.linearIndependent_left`, `perfectClosure.isPurelyInseparable`, `IntermediateField.isSeparable_adjoin_iff_isSeparable`, `NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal`, `IntermediateField.sepDegree_top`, `IsGaloisGroup.fixedPoints_eq_bot`, `IntermediateField.adjoin_contains_field_as_subfield`, `IntermediateField.extendScalars_le_extendScalars_iff`, `IntermediateField.coe_one`

---

← Back to Index