| Name | Category | Theorems |
|---|
algebra' 📖 | CompOp | 283 mathmath: AdjoinSimple.trace_gen_eq_sum_roots, finInsepDegree_top, Field.Emb.Cardinal.equivLim_coherence, InfiniteGalois.normal_iff_isGalois, exists_algHom_adjoin_of_splits, aeval_gen_minpoly, LinearDisjoint.iff_inf_eq_bot, normal_inf, algHomEquivAlgHomOfSplits_symm_apply, algHomEquivAlgHomOfSplits_apply_apply, coe_algebraMap_over_bot, instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic, RatFunc.algEquivOfTranscendental_X, minpoly.algEquiv_apply, isScalarTower_mid', adjoinRootEquivAdjoin_symm_apply_gen, isCyclotomicExtension_singleton_iff_eq_adjoin, isPurelyInseparable_iSup, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField, lift_insepDegree_bot', Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, Field.Emb.Cardinal.filtration_succ, InfiniteGalois.normalAutEquivQuotient_apply, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax, isAlgebraic_tower_bot, algHomEquivAlgHomOfSplits_apply, botEquiv_symm, isGalois_iff_isGalois_top, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, exists_algHom_of_adjoin_splits, normal_iff_forall_map_eq, restrictScalars_normal, isScalarTower, Algebra.FormallySmooth.adjoin_of_algebraicIndependent, isPurelyInseparable_iff_fd_isPurelyInseparable, LinearDisjoint.of_isField', PowerBasis.equivAdjoinSimple_symm_aeval, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, lift_adjoin_simple, algebraicClosure.normalClosure_eq_self, AdjoinDouble.normal_algebraicClosure, algebraicClosure.isAlgebraic, IsGalois.normalClosure, isAlgebraic_iff, RatFunc.Luroth.algEquiv_apply, coe_inclusion, LinearDisjoint.of_le, IsGaloisGroup.quotientMap, LinearDisjoint.trace_algebraMap, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, minpoly_gen, aeval_coe, Field.Emb.Cardinal.succEquiv_coherence, finSepDegree_adjoin_simple_eq_finrank_iff, linearDisjoint_comm, Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, equivOfEq_symm, restrictRestrictAlgEquivMapHom_apply, fieldRange_comp_val, adjoin.powerBasis_gen, equivOfEq_rfl, normal_iff_normalClosure_le, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, IsGaloisGroup.quotient, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, normal_iSup, restrictRestrictAlgEquivMapHom_surjective, IsGaloisGroup.instSMulCommClassQuotientSubgroupSubtypeMemIntermediateField, AdjoinSimple.norm_gen_eq_one, range_val, isCyclotomicExtension_lcm_sup, linearDisjoint_iff', splits_iff_mem, Algebra.normalizedTrace_intermediateField, isNormalClosure_normalClosure, lift_top, insepDegree_bot', exists_algHom_adjoin_of_splits_of_aeval, AlgebraicIndependent.lift_reprField, isAlgebraic_adjoin, instIsLiouvilleSubtypeMemIntermediateField, RatFunc.Luroth.algEquiv_algebraMap, PowerBasis.equivAdjoinSimple_aeval, isPurelyInseparable_tower_bot, le_separableClosure_iff, RatFunc.algEquivOfTranscendental_symm_gen, botContinuousSMul, LinearDisjoint.of_le_right, eq_separableClosure_iff, normal_iff_forall_fieldRange_le, IsGalois.normalAutEquivQuotient_apply, trace_eq_trace_adjoin, coe_isIntegral_iff, Submodule.traceDual_le_span_map_traceDual, InfiniteGalois.proj_adjoin_singleton_val, lift_inf, IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank, exists_finset_of_mem_supr'', exists_algHom_of_splits, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1, PowerBasis.equivAdjoinSimple_gen, Field.Emb.Cardinal.equivSucc_coherence, restrictScalars_adjoin_eq_sup, FiniteGaloisIntermediateField.isGalois, Lifts.lt_iff, extendScalars_le_iff, instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, Splits.algebraicClosure, PowerBasis.equivAdjoinSimple_symm_gen, coe_val, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable', restrictRestrictAlgEquivMapHom_injective, normal_iff_forall_map_le', normal_iff_forall_fieldRange_eq, InfiniteGalois.restrict_fixedField, sepDegree_bot, normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure, finInsepDegree_bot', RatFunc.minpolyX_aeval_X, RatFunc.algEquivOfTranscendental_symm_aeval, Algebra.norm_eq_norm_adjoin, isAlgebraic_adjoin_iff_isAlgebraic, LinearDisjoint.norm_algebraMap, restrictScalars_bot_eq_self, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable, mem_lift, isAlgebraic_adjoin_pair, adjoinRootEquivAdjoin_apply_root, normalClosureOperator_apply, finSepDegree_adjoin_simple_eq_natSepDegree, isPurelyInseparable_adjoin_iff_pow_mem, le_restrictScalars_separableClosure, instIsScalarTowerSubtypeMem_1, RatFunc.irreducible_minpolyX, LinearDisjoint.of_basis_right, lift_injective, RatFunc.Luroth.algEquiv_X, isSeparable_adjoin_simple_iff_isSeparable, AdjoinSimple.trace_gen_eq_zero, lift_sepDegree_bot', RatFunc.natDegree_minpolyX, finSepDegree_adjoin_simple_le_finrank, card_algHom_adjoin_integral, LinearDisjoint.of_inf_eq_bot, AlgebraicIndependent.liftAlgHom_comp_reprField, inclusion_self, lift_bot, normalClosure_of_normal, RatFunc.minpolyX_eq_zero_iff, isSplittingField_iSup, algHomAdjoinIntegralEquiv_symm_apply_gen, le_extendScalars_iff, extendScalars.orderIso_symm_apply_coe, sepDegree_bot', inclusion_injective, Differential.instDifferentialAlgebraSubtypeMemIntermediateField, LinearDisjoint.bot_right, normal_iff_forall_map_le, separableClosure.isAlgebraic, spectralNorm.eq_of_normalClosure, LinearDisjoint.linearIndependent_right, spectralNorm.eq_of_normalClosure', separableClosure.isSepClosure, InfiniteGalois.toAlgEquivAux_eq_liftNormal, normalClosure_def'', Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint, AdjoinSimple.norm_gen_eq_prod_roots, isSeparable_tower_bot, minpoly_eq, isSplittingField_iff, topEquiv_symm_apply_coe, FiniteGaloisIntermediateField.adjoin_val, isAlgebraic_adjoin_simple, AdjoinSimple.normal_algebraicClosure, normal_iff_forall_map_eq', intermediateFieldMap_apply_coe, topEquiv_apply, LinearDisjoint.symm, exists_algHom_adjoin_of_splits', Algebra.normalizedTrace_def, AdjoinSimple.isIntegral_gen, RatFunc.natDegree_num_le_natDegree_minpolyX, normal_iInf, Algebra.IsAlgebraic.isNormalClosure_normalClosure, isPurelyInseparable_bot, AlgebraicIndependent.aevalEquivField_apply_coe, LinearDisjoint.exists_field_of_isDomain, isSeparable_adjoin_pair_of_isSeparable, le_perfectClosure_iff, perfectClosure.isAlgebraic, isSeparable_sup, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, InfiniteGalois.restrictNormalHom_continuous, isAlgebraic_iSup, IsGalois.of_separable_splitting_field_aux, coe_equivMap_apply, finInsepDegree_bot, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot, isSeparable_iSup, krullTopology_mem_nhds_one_iff_of_normal, isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, separableClosure.isSeparable, botEquiv_def, le_algebraicClosure_iff, adjoin_adjoin_comm, finSepDegree_bot', val_mk, AlgEquiv.restrictNormalHom_apply, InfiniteGalois.mk_toAlgEquivAux, instIsAbelianGaloisSubtypeMemIntermediateField, adjoin_simple_comm, algebraicClosure.isAlgClosure, inclusion_inclusion, extendScalars_restrictScalars, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin, RatFunc.C_minpolyX, InfiniteGalois.proj_of_le, lift_adjoin, LinearDisjoint.of_finrank_sup, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, lift_sup, normalClosure.normal, adjoin_adjoin_left, normalClosure_mono, AdjoinSimple.coe_aeval_gen_apply, restrictNormalHom_ker, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin, insepDegree_bot, equivOfEq_apply, isAlgebraic_adjoin_iff_bot, fieldRange_val, liftAlgEquiv_apply, LinearDisjoint.of_basis_mul, insepDegree_top, separableClosure_le_separableClosure_iff, RatFunc.algEquivOfTranscendental_algebraMap, finSepDegree_top, normalClosure_le_iff_of_normal, AlgHom.fieldRange_of_normal, Lifts.eq_iff, normalClosure_map_eq, IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension, le_normalClosure, equivOfEq_trans, normalClosure_def', Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, mem_restrict, LinearDisjoint.isDomain, RatFunc.natDegree_denom_le_natDegree_minpolyX, isGalois_bot, intermediateFieldMap_symm_apply_coe, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, normal_sup, coe_algebraMap_apply, separableClosure.isGalois, isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one, restrictScalars_adjoin, LinearDisjoint.map, RatFunc.algEquivOfTranscendental_apply, Lifts.le_iff, trace_adjoinSimpleGen, normal_iff_normalClosure_eq, isIntegral_iff, LinearDisjoint.isField_of_isAlgebraic, separableClosure.normalClosure_eq_self, adjoin.powerBasis_dim, IsGalois.of_fixedField_normal_subgroup, essFiniteType_iff, Field.Emb.cardinal_separableClosure, isPurelyInseparable_sup, splits_of_splits, isPurelyInseparable_adjoin_simple_iff_pow_mem, adjoin_rootSet_isSplittingField, nonempty_algHom_adjoin_of_splits, isScalarTower_mid, finSepDegree_bot, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed, LinearDisjoint.linearIndependent_left, perfectClosure.isPurelyInseparable, isSeparable_adjoin_iff_isSeparable, sepDegree_top
|
comap 📖 | CompOp | 24 mathmath: relrank_comap_comap_eq_relrank_inf, relfinrank_comap, map_le_iff_le_comap, map_comap_eq_self_of_surjective, relfinrank_comap_comap_eq_relfinrank_of_le, map_comap_eq_self, relrank_comap, lift_relrank_comap, gc_map_comap, map_comap_eq, relrank_comap_comap_eq_relrank_of_le, finrank_comap, lift_relrank_comap_comap_eq_lift_relrank_of_le, relfinrank_comap_comap_eq_relfinrank_of_surjective, lift_relrank_comap_comap_eq_lift_relrank_inf, separableClosure.comap_eq_of_algHom, lift_relrank_comap_comap_eq_lift_relrank_of_surjective, rank_comap, relfinrank_comap_comap_eq_relfinrank_inf, lift_rank_comap, relrank_comap_comap_eq_relrank_of_surjective, comap_map, algebraicClosure.comap_eq_of_algHom, perfectClosure.comap_eq_of_algHom
|
copy 📖 | CompOp | 2 mathmath: copy_eq, coe_copy
|
equivMap 📖 | CompOp | 1 mathmath: coe_equivMap_apply
|
equivOfEq 📖 | CompOp | 4 mathmath: equivOfEq_symm, equivOfEq_rfl, equivOfEq_apply, equivOfEq_trans
|
extendScalars 📖 | CompOp | 22 mathmath: extendScalars_toSubfield, extendScalars_sup, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right, extendScalars_injective, extendScalars.orderIso_apply, extendScalars_adjoin, extendScalars_inf, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, extendScalars_self, extendScalars_le_iff, coe_extendScalars, le_extendScalars_iff, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left, relfinrank_eq_finrank_of_le, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, extendScalars_restrictScalars, mem_extendScalars, relrank_eq_rank_of_le, extendScalars_top, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic, extendScalars_le_extendScalars_iff
|
inclusion 📖 | CompOp | 9 mathmath: exists_algHom_adjoin_of_splits, coe_inclusion, IsGaloisGroup.quotientMap, Lifts.lt_iff, inclusion_self, inclusion_injective, inclusion_inclusion, Lifts.eq_iff, Lifts.le_iff
|
instAlgebraSubtypeMem 📖 | CompOp | 125 mathmath: extendScalars_toSubfield, LinearDisjoint.iff_inf_eq_bot, IsGalois.tower_top_intermediateField, algHomEquivAlgHomOfSplits_apply_apply, extendScalars_sup, Field.Emb.Cardinal.filtration_succ, algebraicClosure.algebraicClosure_eq_bot, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right, InfiniteGalois.normalAutEquivQuotient_apply, RatFunc.IntermediateField.adjoin_X, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, extendScalars_injective, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, LinearDisjoint.of_isField', isAlgebraic_adjoin_iff_top, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', LinearDisjoint.of_le, LinearDisjoint.trace_algebraMap, Field.Emb.Cardinal.two_le_deg, finInsepDegree_le_of_left_le, isAlgebraic_adjoin_iff, RatFunc.IntermediateField.isAlgebraic_X, Field.Emb.Cardinal.succEquiv_coherence, linearDisjoint_comm, IsGaloisGroup.of_fixedPoints_eq, restrictRestrictAlgEquivMapHom_apply, IsGalois.sup_right, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, normalClosure.restrictScalars_eq, restrictRestrictAlgEquivMapHom_surjective, linearDisjoint_iff', extendScalars.orderIso_apply, LinearDisjoint.basisOfBasisLeft_apply, algebraicClosure.isIntegralClosure, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, LinearDisjoint.basisOfBasisRight_apply, IsTranscendenceBasis.isAlgebraic_field, extendScalars_adjoin, extendScalars_inf, botContinuousSMul, LinearDisjoint.of_le_right, eq_separableClosure_iff, IsGalois.normalAutEquivQuotient_apply, isAlgebraic_tower_top, Submodule.traceDual_le_span_map_traceDual, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, extendScalars_self, restrictScalars_adjoin_eq_sup, extendScalars_le_iff, restrictRestrictAlgEquivMapHom_injective, Transcendental.algebraicClosure, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, instIsAbelianGaloisSubtypeMemIntermediateField_1, InfiniteGalois.restrict_fixedField, instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois, RatFunc.minpolyX_aeval_X, LinearDisjoint.norm_algebraMap, restrictScalars_bot_eq_self, Differential.instDifferentialAlgebraSubtypeMemIntermediateField_1, le_restrictScalars_separableClosure, instIsScalarTowerSubtypeMem_1, normal, LinearDisjoint.of_basis_right, isTranscendenceBasis_adjoin_iff, coe_extendScalars, AdjoinPair.algebraMap_gen₁, LinearDisjoint.of_inf_eq_bot, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top, Field.Emb.Cardinal.deg_lt_aleph0, le_extendScalars_iff, extendScalars.orderIso_symm_apply_coe, exists_isTranscendenceBasis_and_isSeparable_of_perfectField, IsGaloisGroup.subgroup_iff, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left, LinearDisjoint.bot_right, IsGaloisGroup.intermediateField, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, spectralNorm.eq_of_normalClosure', InfiniteGalois.toAlgEquivAux_eq_liftNormal, Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint, relfinrank_eq_finrank_of_le, adjoin_eq_range_algebraMap_adjoin, LinearDisjoint.symm, LinearDisjoint.exists_field_of_isDomain, InfiniteGalois.restrictNormalHom_continuous, IsGaloisGroup.subgroup, RatFunc.isAlgebraic_adjoin_simple_X', adjoin_adjoin_comm, AlgebraicIndependent.algebraicClosure, AlgEquiv.restrictNormalHom_apply, adjoin_simple_comm, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, extendScalars_restrictScalars, mem_extendScalars, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow, adjoin_minpoly_coeff_of_exists_primitive_element, relrank_eq_rank_of_le, extendScalars_top, algebraicIndependent_adjoin_iff, LinearDisjoint.of_finrank_sup, adjoin_adjoin_left, separableClosure_le_iff, LinearDisjoint.basisOfBasisLeft_repr_apply, restrictNormalHom_ker, LinearDisjoint.of_basis_mul, separableClosure_le_separableClosure_iff, transcendental_adjoin_iff, separableClosure.separableClosure_eq_bot, instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, RatFunc.isAlgebraic_adjoin_simple_X, isPurelyInseparable_tower_top, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, isGalois_iff_isGalois_bot, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic, Field.insepDegree_le_of_left_le, restrictScalars_adjoin, LinearDisjoint.map, isSeparable_tower_top, AdjoinPair.algebraMap_gen₂, AdjoinSimple.algebraMap_gen, separableClosure.isPurelyInseparable, extendScalars_le_extendScalars_iff
|
instAlgebraSubtypeMem_1 📖 | CompOp | 4 mathmath: Field.Emb.Cardinal.two_le_deg, Field.Emb.Cardinal.succEquiv_coherence, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, Field.Emb.Cardinal.deg_lt_aleph0
|
instDistribMulActionSubtypeMem 📖 | CompOp | — |
instModuleSubtypeMem 📖 | CompOp | 43 mathmath: LinearDisjoint.linearIndependent_right', relfinrank_mul_finrank_top, relrank_mul_rank_top, IsGalois.card_fixingSubgroup_eq_finrank, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, finiteDimensional_right, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic, relfinrank_top_right, relrank_top_right, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right, LinearDisjoint.basisOfBasisLeft_apply, finrank_lt_of_gt, LinearDisjoint.basisOfBasisRight_apply, LinearDisjoint.finrank_right_eq_finrank, trace_eq_finrank_mul_minpoly_nextCoeff, rank_top, trace_eq_trace_adjoin, finrank_top, LinearDisjoint.finrank_left_eq_finrank, RatFunc.finrank_eq_max_natDegree, finrank_eq_one_iff_eq_top, trace_eq_sum_roots, Algebra.norm_eq_norm_adjoin, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right, relrank_dvd_rank_top_of_le, LinearDisjoint.linearIndependent_right, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, finrank_fixedField_eq_card, finrank_comap, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left, relfinrank_dvd_finrank_top_of_le, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left, finrank_le_of_le_left, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, finrank_bot', Algebra.norm_eq_prod_roots, LinearDisjoint.basisOfBasisLeft_repr_apply, rank_bot', rank_comap, lift_rank_comap, IsGaloisGroup.card_fixingSubgroup_eq_finrank, IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, finrank_dvd_of_le_left
|
instModuleSubtypeMem_1 📖 | CompOp | 9 mathmath: LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left, relfinrank_eq_finrank_of_le, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, relrank_eq_rank_of_le, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic
|
instMulActionSubtypeMem 📖 | CompOp | — |
instMulActionWithZeroSubtypeMem 📖 | CompOp | — |
instMulDistribMulActionSubtypeMem 📖 | CompOp | — |
instMulSemiringActionSubtypeMem 📖 | CompOp | — |
instPartialOrder 📖 | CompOp | 100 mathmath: normalClosure_le_iff, Field.Emb.Cardinal.equivLim_coherence, map_mono, lift_le, perfectClosure.map_le_of_algHom, mem_subalgebraEquivIntermediateField, map_le_iff_le_comap, Field.Emb.Cardinal.directed_filtration, Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, isCyclotomicExtension_le_of_dvd, relrank_eq_one_iff, extendScalars_injective, adjoin_simple_isCompactElement, adjoin.mono, adjoin_finite_isCompactElement, adjoin_le_iff, Field.Emb.Cardinal.succEquiv_coherence, IsGalois.intermediateFieldEquivSubgroup_apply, Subfield.extendScalars_le_extendScalars_iff, normal_iff_normalClosure_le, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, extendScalars.orderIso_apply, IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup, solvableByRad_le, fixedField_antitone, mem_subalgebraEquivIntermediateField_symm, le_separableClosure_iff, separableClosure_le, restrictScalars_le_iff, separableClosure.map_le_of_algHom, normal_iff_forall_fieldRange_le, extendScalars_self, Subfield.extendScalars.orderIso_symm_apply, Field.Emb.Cardinal.equivSucc_coherence, le_algebraicClosure, Lifts.lt_iff, extendScalars_le_iff, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual, algebraicClosure.map_le_of_algHom, normal_iff_forall_map_le', fixingSubgroup_antitone, algebraicClosure.le_restrictScalars, adjoin_simple_le_iff, le_perfectClosure, normalClosureOperator_apply, Field.Emb.Cardinal.eq_bot_of_not_nonempty, le_restrictScalars_separableClosure, Field.Emb.Cardinal.filtration_apply, gc_map_comap, Subfield.le_extendScalars_iff, IsGalois.intermediateFieldEquivSubgroup_symm_apply, inclusion_self, le_extendScalars_iff, Subfield.extendScalars_le_iff, extendScalars.orderIso_symm_apply_coe, solvableByRad_le_algClosure, normal_iff_forall_map_le, normalClosureOperator_isClosed, Subfield.extendScalars.orderIso_apply, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply, algebraicClosure.adjoin_le, Field.Emb.Cardinal.strictMono_filtration, adjoin_finset_isCompactElement, le_perfectClosure_iff, AlgHom.fieldRange_le_normalClosure, RatFunc.Luroth.adjoin_generator_le, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, le_algebraicClosure_iff, toSubalgebra_lt_toSubalgebra, fixedField_le, inclusion_inclusion, le_iff_le, IsGaloisGroup.fixedPoints_le_of_le, extendScalars_top, le_separableClosure', toSubalgebra_strictMono, normalClosure_mono, separableClosure_le_iff, isClosed_restrictScalars_separableClosure, gc, FiniteGaloisIntermediateField.le_iff, separableClosure_le_separableClosure_iff, Field.Emb.Cardinal.iSup_filtration, isSimpleOrder_of_finrank_prime, le_separableClosure, toSubalgebra_le_toSubalgebra, normalClosure_le_iff_of_normal, Lifts.eq_iff, le_normalClosure, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, Lifts.le_iff, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin, relfinrank_eq_one_iff, IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual, separableClosure.adjoin_le, separableClosure.le_restrictScalars, le_algebraicClosure', IsGalois.ofDual_intermediateFieldEquivSubgroup_apply, extendScalars_le_extendScalars_iff
|
instSMulSubtypeMem 📖 | CompOp | 15 mathmath: isScalarTower_mid', smulCommClass_left, instIsScalarTowerSubtypeMem, isScalarTower_bot, continuousSMul, instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap, normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1, instFaithfulSMulSubtypeMem, isScalarTower_over_bot, smul_def, fixedField.isScalarTower, smulCommClass_right, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap, isScalarTower_mid
|
instSMulSubtypeMem_1 📖 | CompOp | 1 mathmath: instIsScalarTowerSubtypeMem_1
|
instSMulWithZeroSubtypeMem 📖 | CompOp | — |
instSetLike 📖 | CompOp | 630 mathmath: IsGaloisGroup.smul_mem_of_normal, extendScalars_toSubfield, AdjoinSimple.trace_gen_eq_sum_roots, finInsepDegree_top, Field.Emb.Cardinal.equivLim_coherence, InfiniteGalois.normal_iff_isGalois, exists_algHom_adjoin_of_splits, mem_perfectClosure_iff_natSepDegree_eq_one, aeval_gen_minpoly, LinearDisjoint.iff_inf_eq_bot, normal_inf, algHomEquivAlgHomOfSplits_symm_apply, IsGalois.tower_top_intermediateField, LinearDisjoint.linearIndependent_right', adjoin.finrank, algebraMap_mem, adjoin_intermediateField_toSubalgebra_of_isAlgebraic, algHomEquivAlgHomOfSplits_apply_apply, extendScalars_sup, coe_algebraMap_over_bot, instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic, RatFunc.algEquivOfTranscendental_X, mem_subalgebraEquivIntermediateField, minpoly.algEquiv_apply, isScalarTower_mid', adjoinRootEquivAdjoin_symm_apply_gen, isCyclotomicExtension_singleton_iff_eq_adjoin, isPurelyInseparable_iSup, coe_prod, coe_bot, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField, FiniteGaloisIntermediateField.subset_adjoin, lift_insepDegree_bot', Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, Field.Emb.Cardinal.filtration_succ, relfinrank_mul_finrank_top, algebraicClosure.algebraicClosure_eq_bot, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right, coe_iSup_of_directed, InfiniteGalois.normalAutEquivQuotient_apply, IsGaloisGroup.fixingSubgroup_top, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax, isAlgebraic_tower_bot, mem_adjoin_iff, mem_carrier, algHomEquivAlgHomOfSplits_apply, botEquiv_symm, relrank_mul_rank_top, IsGalois.card_fixingSubgroup_eq_finrank, Subfield.relfinrank_eq_finrank_of_le, NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow, isGalois_iff_isGalois_top, RatFunc.IntermediateField.adjoin_X, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, InfiniteGalois.mem_bot_iff_fixed, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, exists_algHom_of_adjoin_splits, normal_iff_forall_map_eq, extendScalars_injective, ext_iff, natCast_mem, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic, coe_neg, restrictScalars_normal, isScalarTower, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, Algebra.FormallySmooth.adjoin_of_algebraicIndependent, algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, isPurelyInseparable_iff_fd_isPurelyInseparable, LinearDisjoint.of_isField', coe_iInf, PowerBasis.equivAdjoinSimple_symm_aeval, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, Subfield.coe_toIntermediateField, lift_adjoin_simple, algebraicClosure.normalClosure_eq_self, AdjoinDouble.normal_algebraicClosure, coe_add, mem_adjoin_simple_self, prod_mem, isAlgebraic_adjoin_iff_top, algebraicClosure.isAlgebraic, IsGalois.normalClosure, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', finiteDimensional_right, isAlgebraic_iff, RatFunc.Luroth.algEquiv_apply, charZero, NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic, mem_adjoin_of_mem, subset_adjoin_of_subset_left, instSMulMemClass, coe_inclusion, adjoin_le_iff, finiteDimensional_iSup_of_finset, LinearDisjoint.of_le, IsGaloisGroup.quotientMap, LinearDisjoint.trace_algebraMap, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, Field.Emb.Cardinal.two_le_deg, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic, div_mem, smulCommClass_left, finInsepDegree_le_of_left_le, isAlgebraic_adjoin_iff, minpoly_gen, Field.Emb.Cardinal.isLeast_leastExt, aeval_coe, instIsScalarTowerSubtypeMem, RatFunc.IntermediateField.isAlgebraic_X, IsKrasner.krasner', coe_toSubalgebra, Field.Emb.Cardinal.succEquiv_coherence, isScalarTower_bot, relfinrank_top_right, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, finSepDegree_adjoin_simple_eq_finrank_iff, linearDisjoint_comm, IsGaloisGroup.of_fixedPoints_eq, Lifts.exists_lift_of_splits', Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, equivOfEq_symm, coe_type_toSubfield, restrictRestrictAlgEquivMapHom_apply, mem_top, fieldRange_comp_val, adjoin.powerBasis_gen, equivOfEq_rfl, normal_iff_normalClosure_le, mem_perfectClosure_iff_pow_mem, relrank_top_right, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, isTotallyReal_bot, continuousSMul, IsGaloisGroup.quotient, relfinrank_dvd_finrank_bot, IsGalois.sup_right, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, normalClosure.restrictScalars_eq, normal_iSup, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right, mem_adjoin_pair_right, restrictRestrictAlgEquivMapHom_surjective, IsGaloisGroup.instSMulCommClassQuotientSubgroupSubtypeMemIntermediateField, multiset_prod_mem, AdjoinSimple.norm_gen_eq_one, range_val, instFiniteSubtypeMemBot, isCyclotomicExtension_lcm_sup, LinearDisjoint.linearIndependent_mul, map_mem_perfectClosure_iff, linearDisjoint_iff', IsGaloisGroup.fixedPoints_fixingSubgroup, splits_iff_mem, extendScalars.orderIso_apply, LinearDisjoint.basisOfBasisLeft_apply, algebraicClosure.isIntegralClosure, Algebra.normalizedTrace_intermediateField, add_mem, IsGaloisGroup.le_fixedPoints_iff_le_fixingSubgroup, isNormalClosure_normalClosure, mem_fixedField_iff, finrank_eq_one_iff, lift_top, IsGaloisGroup.fixingSubgroup_le_of_le, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, finrank_lt_of_gt, map_mem_separableClosure_iff, insepDegree_bot', exists_algHom_adjoin_of_splits_of_aeval, LinearDisjoint.basisOfBasisRight_apply, AlgebraicIndependent.lift_reprField, isAlgebraic_adjoin, mem_subalgebraEquivIntermediateField_symm, instIsLiouvilleSubtypeMemIntermediateField, coe_mul, sSup_def, IsTranscendenceBasis.isAlgebraic_field, RatFunc.Luroth.algEquiv_algebraMap, Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, PowerBasis.equivAdjoinSimple_aeval, extendScalars_adjoin, isPurelyInseparable_tower_bot, neg_mem, le_separableClosure_iff, charP', RatFunc.algEquivOfTranscendental_symm_gen, toIntermediateField'_toSubalgebra, RatFunc.Luroth.generator_mem, extendScalars_inf, botContinuousSMul, LinearDisjoint.of_le_right, eq_separableClosure_iff, mem_toSubfield, mem_algebraicClosure_iff, normal_iff_forall_fieldRange_le, IsGalois.normalAutEquivQuotient_apply, instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap, LinearDisjoint.finrank_right_eq_finrank, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, instSubfieldClass, trace_eq_finrank_mul_minpoly_nextCoeff, rank_adjoin_eq_one_iff, normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1, isAlgebraic_tower_top, rank_top, finrank_eq_fixingSubgroup_index, trace_eq_trace_adjoin, coe_isIntegral_iff, Submodule.traceDual_le_span_map_traceDual, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, IsGaloisGroup.fixingSubgroup_fixedPoints, InfiniteGalois.proj_adjoin_singleton_val, lift_inf, IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank, mem_perfectClosure_iff, smul_mem, exists_finset_of_mem_supr'', exists_algHom_of_splits, extendScalars_self, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1, PowerBasis.equivAdjoinSimple_gen, coe_inf, Field.Emb.Cardinal.equivSucc_coherence, finrank_top, restrictScalars_adjoin_eq_sup, FiniteGaloisIntermediateField.isGalois, mem_adjoin_iff_div, LinearDisjoint.finrank_left_eq_finrank, Lifts.lt_iff, mem_inf, extendScalars_le_iff, instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, cardinalMk_adjoin_le, coe_sum, Splits.algebraicClosure, PowerBasis.equivAdjoinSimple_symm_gen, coe_val, RatFunc.finrank_eq_max_natDegree, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, finrank_eq_finrank_subalgebra, finrank_eq_one_iff_eq_top, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable', restrictRestrictAlgEquivMapHom_injective, list_sum_mem, Transcendental.algebraicClosure, coe_toSubfield, LinearDisjoint.finrank_sup, finrank_adjoin_eq_one_iff, Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, normal_iff_forall_map_le', normal_iff_forall_fieldRange_eq, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, instIsAbelianGaloisSubtypeMemIntermediateField_1, instFaithfulSMulSubtypeMem, finrank_bot, InfiniteGalois.restrict_fixedField, instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois, subset_adjoin_of_subset_right, sepDegree_bot, normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure, trace_eq_sum_roots, algebraMap_apply, exists_finset_of_mem_iSup, adjoin_simple_le_iff, finInsepDegree_bot', RatFunc.minpolyX_aeval_X, RatFunc.algEquivOfTranscendental_symm_aeval, Algebra.norm_eq_norm_adjoin, subset_adjoin, isAlgebraic_adjoin_iff_isAlgebraic, LinearDisjoint.norm_algebraMap, restrictScalars_bot_eq_self, adjoin.range_algebraMap_subset, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable, sup_def, mem_lift, isAlgebraic_adjoin_pair, finrank_sup_le, Differential.instDifferentialAlgebraSubtypeMemIntermediateField_1, list_prod_mem, adjoinRootEquivAdjoin_apply_root, normalClosureOperator_apply, finSepDegree_adjoin_simple_eq_natSepDegree, rank_bot, isPurelyInseparable_adjoin_iff_pow_mem, le_restrictScalars_separableClosure, coe_zero, separableClosure.adjoin_eq_of_isAlgebraic, adjoin.algebraMap_mem, coe_restrictScalars, instIsScalarTowerSubtypeMem_1, normal, finrank_bot_mul_relfinrank, RatFunc.irreducible_minpolyX, IsIntegral.mem_intermediateField_of_minpoly_splits, LinearDisjoint.of_basis_right, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right, finiteDimensional_adjoin, isTranscendenceBasis_adjoin_iff, adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left, lift_injective, adjoin_eq_bot_iff, RatFunc.Luroth.algEquiv_X, coe_extendScalars, isSeparable_adjoin_simple_iff_isSeparable, AdjoinSimple.trace_gen_eq_zero, lift_sepDegree_bot', mem_adjoin_range_iff, relrank_dvd_rank_top_of_le, RatFunc.natDegree_minpolyX, algebraAdjoinAdjoin.algebraMap_eq_gen_self, finSepDegree_adjoin_simple_le_finrank, card_algHom_adjoin_integral, relrank_dvd_rank_bot, AdjoinPair.algebraMap_gen₁, sub_mem, NumberField.finite_of_discr_bdd, LinearDisjoint.of_inf_eq_bot, AlgHom.coe_fieldRange, AlgebraicIndependent.liftAlgHom_comp_reprField, finrank_top', exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top, inclusion_self, lift_bot, normalClosure_of_normal, charP, intCast_mem, RatFunc.minpolyX_eq_zero_iff, InfiniteGalois.isOpen_iff_finite, isSplittingField_iSup, Field.Emb.Cardinal.deg_lt_aleph0, algHomAdjoinIntegralEquiv_symm_apply_gen, adjoin_simple_eq_bot_iff, relfinrank_bot_left, solvableByRad.rad_mem, iSup_eq_adjoin, LinearDisjoint.rank_sup, le_extendScalars_iff, rank_sup_le_of_isAlgebraic, extendScalars.orderIso_symm_apply_coe, exists_isTranscendenceBasis_and_isSeparable_of_perfectField, sepDegree_bot', Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, inclusion_injective, Differential.instDifferentialAlgebraSubtypeMemIntermediateField, IsGaloisGroup.subgroup_iff, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left, LinearDisjoint.bot_right, normal_iff_forall_map_le, separableClosure.isAlgebraic, expChar, rank_eq_one_iff, IsGaloisGroup.intermediateField, adjoin_rank_le_of_isAlgebraic_right, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_left, spectralNorm.eq_of_normalClosure, LinearDisjoint.linearIndependent_right, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, mem_adjoin_pair_left, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, spectralNorm.eq_of_normalClosure', algebraicClosure.adjoin_le, AlgHom.mem_fieldRange, finrank_fixedField_eq_card, separableClosure.isSepClosure, finrank_comap, InfiniteGalois.toAlgEquivAux_eq_liftNormal, normalClosure_def'', Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint, AdjoinSimple.norm_gen_eq_prod_roots, Subfield.relrank_eq_rank_of_le, relfinrank_eq_finrank_of_le, FixedBy.intermediateField_mem_iff, isScalarTower_over_bot, isSeparable_tower_bot, minpoly_eq, exists_finset_of_mem_adjoin, IsGaloisGroup.coe_quotient_smul, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left, mem_toSubalgebra, isSplittingField_iff, topEquiv_symm_apply_coe, FiniteGaloisIntermediateField.adjoin_val, NumberField.of_intermediateField, adjoin_eq_range_algebraMap_adjoin, multiset_sum_mem, rank_top', isAlgebraic_adjoin_simple, exists_finset_of_mem_supr', AdjoinSimple.normal_algebraicClosure, normal_iff_forall_map_eq', intermediateFieldMap_apply_coe, topEquiv_apply, LinearDisjoint.symm, exists_algHom_adjoin_of_splits', Algebra.normalizedTrace_def, coe_inv, AdjoinSimple.isIntegral_gen, RatFunc.natDegree_num_le_natDegree_minpolyX, map_mem_algebraicClosure_iff, mem_restrictScalars, mem_sInf, exists_lt_finrank_of_infinite_dimensional, adjoin_rank_le_of_isAlgebraic, normal_iInf, Algebra.IsAlgebraic.isNormalClosure_normalClosure, mul_mem, isPurelyInseparable_bot, mem_algebraicClosure_iff', AlgebraicIndependent.aevalEquivField_apply_coe, LinearDisjoint.exists_field_of_isDomain, adjoin_toSubalgebra_of_isAlgebraic_right, isSeparable_adjoin_pair_of_isSeparable, finiteDimensional_left, finiteDimensional_iSup_of_finite, le_perfectClosure_iff, perfectClosure.isAlgebraic, isSeparable_sup, FiniteGaloisIntermediateField.finiteDimensional, map_mem_map, IsGaloisGroup.smul_eq_self, smul_def, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, coe_smul, IsGaloisGroup.fixingSubgroup_bot, Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, relfinrank_dvd_finrank_top_of_le, set_range_subset, InfiniteGalois.restrictNormalHom_continuous, isAlgebraic_iSup, IsGaloisGroup.subgroup, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left, fixedField.isScalarTower, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, IsGalois.of_separable_splitting_field_aux, coe_equivMap_apply, adjoin_insert_adjoin, mem_adjoin_simple_iff, finrank_le_of_le_left, finInsepDegree_bot, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, krullTopology_mem_nhds_one_iff, one_mem, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, lift_cardinalMk_adjoin_le, isSeparable_iSup, krullTopology_mem_nhds_one_iff_of_normal, finrank_bot', isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, Lifts.exists_lift_of_splits, separableClosure.isSeparable, RatFunc.isAlgebraic_adjoin_simple_X', adjoin_toSubalgebra_of_isAlgebraic_left, Algebra.norm_eq_prod_roots, adjoin.finiteDimensional, botEquiv_def, le_algebraicClosure_iff, adjoin_adjoin_comm, AlgebraicIndependent.algebraicClosure, finSepDegree_bot', val_mk, rank_sup_le, coe_pow, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField, AlgEquiv.restrictNormalHom_apply, InfiniteGalois.mk_toAlgEquivAux, instIsAbelianGaloisSubtypeMemIntermediateField, adjoin_simple_comm, algebraicClosure.isAlgClosure, pow_mem, inclusion_inclusion, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, extendScalars_restrictScalars, zero_mem, adjoin_subset_adjoin_iff, mem_extendScalars, perfectClosure.perfectField, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, mem_mk, RatFunc.C_minpolyX, InfiniteGalois.proj_of_le, expChar', exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow, adjoin_minpoly_coeff_of_exists_primitive_element, coe_type_toSubalgebra, relrank_eq_rank_of_le, lift_adjoin, coe_copy, smulCommClass_right, extendScalars_top, algebraicIndependent_adjoin_iff, mem_separableClosure_iff, rank_eq_rank_subalgebra, LinearDisjoint.of_finrank_sup, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, lift_sup, normalClosure.normal, adjoin_adjoin_left, normalClosure_mono, AdjoinSimple.coe_aeval_gen_apply, LinearDisjoint.linearIndependent_mul', separableClosure_le_iff, LinearDisjoint.basisOfBasisLeft_repr_apply, restrictNormalHom_ker, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin, adjoin_rank_le_of_isAlgebraic_left, algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, insepDegree_bot, equivOfEq_apply, rank_bot', gc, isAlgebraic_adjoin_iff_bot, fieldRange_val, liftAlgEquiv_apply, LinearDisjoint.of_basis_mul, inv_mem, insepDegree_top, separableClosure_le_separableClosure_iff, transcendental_adjoin_iff, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, rank_comap, separableClosure.separableClosure_eq_bot, adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right, rank_bot_mul_relrank, instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois, finiteDimensional_map, RatFunc.algEquivOfTranscendental_algebraMap, finSepDegree_top, lift_rank_comap, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_right, instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap, normalClosure_le_iff_of_normal, AlgHom.fieldRange_of_normal, Lifts.eq_iff, IsGaloisGroup.card_fixingSubgroup_eq_finrank, normalClosure_map_eq, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, relrank_bot_left, IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension, IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Subfield.mem_extendScalars, RatFunc.isAlgebraic_adjoin_simple_X, isPurelyInseparable_tower_top, le_normalClosure, equivOfEq_trans, mem_map, normalClosure_def', adjoin_self, mem_bot, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, mem_restrict, perfectClosure.perfectRing, FixedPoints.mem_intermediateField_iff, LinearDisjoint.isDomain, finrank_dvd_of_le_right, finrank_le_of_le_right, RatFunc.natDegree_denom_le_natDegree_minpolyX, coe_top, AdjoinSimple.coe_gen, isGalois_bot, intermediateFieldMap_symm_apply_coe, finrank_dvd_of_le_left, coe_sInf, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, isGalois_iff_isGalois_bot, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic, Field.insepDegree_le_of_left_le, finiteDimensional_adjoin_pair, IsKrasner.krasner, normal_sup, coe_algebraMap_apply, separableClosure.isGalois, isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one, coe_div, restrictScalars_adjoin, finiteDimensional_iSup_of_finset', finrank_adjoin_simple_eq_one_iff, zsmul_mem, LinearDisjoint.map, isSeparable_tower_top, RatFunc.algEquivOfTranscendental_apply, normalClosure.is_finiteDimensional, finiteDimensional_sup, Lifts.le_iff, trace_adjoinSimpleGen, normal_iff_normalClosure_eq, rank_adjoin_simple_eq_one_iff, algebraAdjoinAdjoin.coe_algebraMap, separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable, AdjoinPair.algebraMap_gen₂, isIntegral_iff, LinearDisjoint.isField_of_isAlgebraic, Subfield.coe_extendScalars, separableClosure.normalClosure_eq_self, IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup, coe_map, adjoin.powerBasis_dim, IsGalois.of_fixedField_normal_subgroup, essFiniteType_iff, Field.Emb.cardinal_separableClosure, AdjoinSimple.algebraMap_gen, isPurelyInseparable_sup, splits_of_splits, separableClosure.adjoin_le, IsGalois.mem_bot_iff_fixed, FiniteGaloisIntermediateField.adjoin_simple_le_iff, sum_mem, separableClosure.isPurelyInseparable, isPurelyInseparable_adjoin_simple_iff_pow_mem, adjoin_rootSet_isSplittingField, nonempty_algHom_adjoin_of_splits, isScalarTower_mid, finSepDegree_bot, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed, LinearDisjoint.linearIndependent_left, perfectClosure.isPurelyInseparable, isSeparable_adjoin_iff_isSeparable, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal, sepDegree_top, adjoin_contains_field_as_subfield, extendScalars_le_extendScalars_iff, coe_one
|
intermediateFieldMap 📖 | CompOp | 2 mathmath: intermediateFieldMap_apply_coe, intermediateFieldMap_symm_apply_coe
|
liftAlgEquiv 📖 | CompOp | 1 mathmath: liftAlgEquiv_apply
|
map 📖 | CompOp | 54 mathmath: map_mono, perfectClosure.map_le_of_algHom, relfinrank_comap, map_le_iff_le_comap, AlgHom.fieldRange_eq_map, map_comap_eq_self_of_surjective, normal_iff_forall_map_eq, LinearDisjoint.map', algebraicClosure.map_eq_of_algebraicClosure_eq_bot, map_map, fieldRange_comp_val, toSubalgebra_map, map_fixingSubgroup, map_comap_eq_self, adjoin_map, relrank_comap, toSubfield_map, separableClosure.map_le_of_algHom, AlgHom.map_fieldRange, lift_relrank_comap, algebraicClosure.map_le_of_algHom, normal_iff_forall_map_le', map_injective, gc_map_comap, map_comap_eq, map_iSup, map_iInf, relfinrank_map_map, map_fixingSubgroup_index, normal_iff_forall_map_le, normalClosure_def'', normal_iff_forall_map_eq', intermediateFieldMap_apply_coe, map_mem_map, coe_equivMap_apply, IsGalois.map_fixingSubgroup, relrank_map_map, separableClosure.map_eq_of_separableClosure_eq_bot, perfectClosure.map_eq_of_algEquiv, algebraicClosure.map_eq_of_algEquiv, map_inf, map_sup, finiteDimensional_map, separableClosure.map_eq_of_algEquiv, lift_relrank_map_map, normalClosure_map_eq, mem_map, normalClosure_def', intermediateFieldMap_symm_apply_coe, map_id, LinearDisjoint.map, comap_map, coe_map, map_bot
|
module' 📖 | CompOp | 73 mathmath: adjoin.finrank, InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic, isScalarTower, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, finiteDimensional_iSup_of_finset, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, finSepDegree_adjoin_simple_eq_finrank_iff, relfinrank_dvd_finrank_bot, instFiniteSubtypeMemBot, LinearDisjoint.basisOfBasisLeft_apply, finrank_eq_one_iff, LinearDisjoint.basisOfBasisRight_apply, LinearDisjoint.finrank_right_eq_finrank, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, rank_adjoin_eq_one_iff, finrank_eq_fixingSubgroup_index, IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank, LinearDisjoint.finrank_left_eq_finrank, finrank_eq_finrank_subalgebra, LinearDisjoint.finrank_sup, finrank_adjoin_eq_one_iff, finrank_bot, finrank_sup_le, rank_bot, finrank_bot_mul_relfinrank, finiteDimensional_adjoin, finSepDegree_adjoin_simple_le_finrank, relrank_dvd_rank_bot, NumberField.finite_of_discr_bdd, finrank_top', InfiniteGalois.isOpen_iff_finite, relfinrank_bot_left, LinearDisjoint.rank_sup, rank_sup_le_of_isAlgebraic, rank_eq_one_iff, adjoin_rank_le_of_isAlgebraic_right, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_left, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, Subfield.relrank_eq_rank_of_le, rank_top', Algebra.normalizedTrace_def, exists_lt_finrank_of_infinite_dimensional, adjoin_rank_le_of_isAlgebraic, finiteDimensional_left, finiteDimensional_iSup_of_finite, FiniteGaloisIntermediateField.finiteDimensional, IsGalois.of_separable_splitting_field_aux, krullTopology_mem_nhds_one_iff, krullTopology_mem_nhds_one_iff_of_normal, adjoin.finiteDimensional, rank_sup_le, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField, rank_eq_rank_subalgebra, LinearDisjoint.basisOfBasisLeft_repr_apply, adjoin_rank_le_of_isAlgebraic_left, rank_bot_mul_relrank, finiteDimensional_map, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_right, relrank_bot_left, LinearDisjoint.isDomain, finrank_dvd_of_le_right, finrank_le_of_le_right, finiteDimensional_adjoin_pair, finiteDimensional_iSup_of_finset', finrank_adjoin_simple_eq_one_iff, normalClosure.is_finiteDimensional, finiteDimensional_sup, rank_adjoin_simple_eq_one_iff, LinearDisjoint.isField_of_isAlgebraic, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal
|
restrict 📖 | CompOp | 2 mathmath: mem_restrict, lift_restrict
|
restrictScalars 📖 | CompOp | 42 mathmath: Field.Emb.Cardinal.filtration_succ, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right, restrictScalars_normal, restrictScalars_sup, restrictScalars_top, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, normalClosure.restrictScalars_eq, restrictScalars_adjoin_of_algEquiv, restrictScalars_eq_top_iff, restrictScalars_le_iff, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, restrictScalars_adjoin_eq_sup, extendScalars_le_iff, restrictScalars_injective, restrictScalars_inf, algebraicClosure.le_restrictScalars, restrictScalars_bot_eq_self, le_restrictScalars_separableClosure, coe_restrictScalars, restrictScalars_toSubfield, le_extendScalars_iff, restrictScalars_inj, extendScalars.orderIso_symm_apply_coe, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left, mem_restrictScalars, restrictScalars_toSubalgebra, IsGalois.of_separable_splitting_field_aux, adjoin_adjoin_comm, adjoin_simple_comm, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, extendScalars_restrictScalars, separableClosure.eq_restrictScalars_of_isSeparable, adjoin_adjoin_left, isClosed_restrictScalars_separableClosure, separableClosure_le_separableClosure_iff, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, algebraicClosure.eq_restrictScalars_of_isAlgebraic, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic, restrictScalars_adjoin, separableClosure.le_restrictScalars
|
restrict_algEquiv 📖 | CompOp | — |
toAlgebra 📖 | CompOp | 1 mathmath: algebraMap_apply
|
toField 📖 | CompOp | 468 mathmath: extendScalars_toSubfield, AdjoinSimple.trace_gen_eq_sum_roots, finInsepDegree_top, Field.Emb.Cardinal.equivLim_coherence, InfiniteGalois.normal_iff_isGalois, exists_algHom_adjoin_of_splits, aeval_gen_minpoly, LinearDisjoint.iff_inf_eq_bot, normal_inf, algHomEquivAlgHomOfSplits_symm_apply, IsGalois.tower_top_intermediateField, LinearDisjoint.linearIndependent_right', adjoin.finrank, algHomEquivAlgHomOfSplits_apply_apply, extendScalars_sup, coe_algebraMap_over_bot, instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic, RatFunc.algEquivOfTranscendental_X, SeparableClosure.isSepClosed, minpoly.algEquiv_apply, isScalarTower_mid', adjoinRootEquivAdjoin_symm_apply_gen, isCyclotomicExtension_singleton_iff_eq_adjoin, isPurelyInseparable_iSup, coe_prod, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateField, lift_insepDegree_bot', Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, Field.Emb.Cardinal.filtration_succ, relfinrank_mul_finrank_top, algebraicClosure.algebraicClosure_eq_bot, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right, InfiniteGalois.normalAutEquivQuotient_apply, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax, isAlgebraic_tower_bot, algHomEquivAlgHomOfSplits_apply, botEquiv_symm, relrank_mul_rank_top, IsGalois.card_fixingSubgroup_eq_finrank, Subfield.relfinrank_eq_finrank_of_le, NumberField.natAbs_discr_eq_natAbs_discr_pow_mul_natAbs_discr_pow, isGalois_iff_isGalois_top, RatFunc.IntermediateField.adjoin_X, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, exists_algHom_of_adjoin_splits, normal_iff_forall_map_eq, extendScalars_injective, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic, restrictScalars_normal, isScalarTower, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, Algebra.FormallySmooth.adjoin_of_algebraicIndependent, algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, isPurelyInseparable_iff_fd_isPurelyInseparable, LinearDisjoint.of_isField', PowerBasis.equivAdjoinSimple_symm_aeval, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, lift_adjoin_simple, algebraicClosure.normalClosure_eq_self, AdjoinDouble.normal_algebraicClosure, isAlgebraic_adjoin_iff_top, algebraicClosure.isAlgebraic, IsGalois.normalClosure, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', finiteDimensional_right, isAlgebraic_iff, RatFunc.Luroth.algEquiv_apply, charZero, NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic, coe_inclusion, finiteDimensional_iSup_of_finset, LinearDisjoint.of_le, IsGaloisGroup.quotientMap, LinearDisjoint.trace_algebraMap, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, Field.Emb.Cardinal.two_le_deg, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic, finInsepDegree_le_of_left_le, isAlgebraic_adjoin_iff, minpoly_gen, aeval_coe, RatFunc.IntermediateField.isAlgebraic_X, Field.Emb.Cardinal.succEquiv_coherence, relfinrank_top_right, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, finSepDegree_adjoin_simple_eq_finrank_iff, linearDisjoint_comm, Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, equivOfEq_symm, restrictRestrictAlgEquivMapHom_apply, fieldRange_comp_val, adjoin.powerBasis_gen, equivOfEq_rfl, normal_iff_normalClosure_le, relrank_top_right, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, isTotallyReal_bot, IsGaloisGroup.quotient, relfinrank_dvd_finrank_bot, IsGalois.sup_right, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, normalClosure.restrictScalars_eq, normal_iSup, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right, restrictRestrictAlgEquivMapHom_surjective, IsGaloisGroup.instSMulCommClassQuotientSubgroupSubtypeMemIntermediateField, AdjoinSimple.norm_gen_eq_one, range_val, instFiniteSubtypeMemBot, isCyclotomicExtension_lcm_sup, linearDisjoint_iff', splits_iff_mem, extendScalars.orderIso_apply, LinearDisjoint.basisOfBasisLeft_apply, Algebra.normalizedTrace_intermediateField, isNormalClosure_normalClosure, finrank_eq_one_iff, lift_top, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, finrank_lt_of_gt, insepDegree_bot', exists_algHom_adjoin_of_splits_of_aeval, LinearDisjoint.basisOfBasisRight_apply, AlgebraicIndependent.lift_reprField, isAlgebraic_adjoin, instIsLiouvilleSubtypeMemIntermediateField, SeparableClosure.hasEnoughRootsOfUnity_pow, IsTranscendenceBasis.isAlgebraic_field, RatFunc.Luroth.algEquiv_algebraMap, PowerBasis.equivAdjoinSimple_aeval, extendScalars_adjoin, isPurelyInseparable_tower_bot, le_separableClosure_iff, charP', RatFunc.algEquivOfTranscendental_symm_gen, extendScalars_inf, botContinuousSMul, LinearDisjoint.of_le_right, eq_separableClosure_iff, normal_iff_forall_fieldRange_le, IsGalois.normalAutEquivQuotient_apply, instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap, LinearDisjoint.finrank_right_eq_finrank, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplex, trace_eq_finrank_mul_minpoly_nextCoeff, rank_adjoin_eq_one_iff, normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1, isAlgebraic_tower_top, rank_top, finrank_eq_fixingSubgroup_index, trace_eq_trace_adjoin, coe_isIntegral_iff, Submodule.traceDual_le_span_map_traceDual, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, InfiniteGalois.proj_adjoin_singleton_val, lift_inf, IsGalois.IntermediateField.AdjoinSimple.card_aut_eq_finrank, exists_finset_of_mem_supr'', exists_algHom_of_splits, extendScalars_self, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1, PowerBasis.equivAdjoinSimple_gen, Field.Emb.Cardinal.equivSucc_coherence, finrank_top, restrictScalars_adjoin_eq_sup, FiniteGaloisIntermediateField.isGalois, LinearDisjoint.finrank_left_eq_finrank, Lifts.lt_iff, extendScalars_le_iff, instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, coe_sum, Splits.algebraicClosure, PowerBasis.equivAdjoinSimple_symm_gen, SeparableClosure.hasEnoughRootsOfUnity, coe_val, RatFunc.finrank_eq_max_natDegree, finrank_eq_finrank_subalgebra, finrank_eq_one_iff_eq_top, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable', restrictRestrictAlgEquivMapHom_injective, Transcendental.algebraicClosure, LinearDisjoint.finrank_sup, finrank_adjoin_eq_one_iff, Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, normal_iff_forall_map_le', normal_iff_forall_fieldRange_eq, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, instIsAbelianGaloisSubtypeMemIntermediateField_1, finrank_bot, InfiniteGalois.restrict_fixedField, instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois, sepDegree_bot, normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure, trace_eq_sum_roots, finInsepDegree_bot', RatFunc.minpolyX_aeval_X, RatFunc.algEquivOfTranscendental_symm_aeval, Algebra.norm_eq_norm_adjoin, isAlgebraic_adjoin_iff_isAlgebraic, LinearDisjoint.norm_algebraMap, restrictScalars_bot_eq_self, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable, mem_lift, isAlgebraic_adjoin_pair, finrank_sup_le, Differential.instDifferentialAlgebraSubtypeMemIntermediateField_1, adjoinRootEquivAdjoin_apply_root, normalClosureOperator_apply, finSepDegree_adjoin_simple_eq_natSepDegree, rank_bot, isPurelyInseparable_adjoin_iff_pow_mem, le_restrictScalars_separableClosure, instIsScalarTowerSubtypeMem_1, normal, finrank_bot_mul_relfinrank, RatFunc.irreducible_minpolyX, LinearDisjoint.of_basis_right, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right, finiteDimensional_adjoin, isTranscendenceBasis_adjoin_iff, lift_injective, RatFunc.Luroth.algEquiv_X, coe_extendScalars, isSeparable_adjoin_simple_iff_isSeparable, AdjoinSimple.trace_gen_eq_zero, lift_sepDegree_bot', relrank_dvd_rank_top_of_le, RatFunc.natDegree_minpolyX, algebraAdjoinAdjoin.algebraMap_eq_gen_self, finSepDegree_adjoin_simple_le_finrank, card_algHom_adjoin_integral, relrank_dvd_rank_bot, NumberField.finite_of_discr_bdd, LinearDisjoint.of_inf_eq_bot, AlgebraicIndependent.liftAlgHom_comp_reprField, finrank_top', exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_adjoin_eq_top, inclusion_self, lift_bot, normalClosure_of_normal, charP, RatFunc.minpolyX_eq_zero_iff, InfiniteGalois.isOpen_iff_finite, isSplittingField_iSup, Field.Emb.Cardinal.deg_lt_aleph0, algHomAdjoinIntegralEquiv_symm_apply_gen, relfinrank_bot_left, LinearDisjoint.rank_sup, le_extendScalars_iff, rank_sup_le_of_isAlgebraic, extendScalars.orderIso_symm_apply_coe, exists_isTranscendenceBasis_and_isSeparable_of_perfectField, sepDegree_bot', Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, inclusion_injective, Differential.instDifferentialAlgebraSubtypeMemIntermediateField, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left, LinearDisjoint.bot_right, normal_iff_forall_map_le, separableClosure.isAlgebraic, expChar, rank_eq_one_iff, adjoin_rank_le_of_isAlgebraic_right, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_left, spectralNorm.eq_of_normalClosure, LinearDisjoint.linearIndependent_right, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, spectralNorm.eq_of_normalClosure', finrank_fixedField_eq_card, separableClosure.isSepClosure, finrank_comap, InfiniteGalois.toAlgEquivAux_eq_liftNormal, normalClosure_def'', Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint, AdjoinSimple.norm_gen_eq_prod_roots, Subfield.relrank_eq_rank_of_le, relfinrank_eq_finrank_of_le, isSeparable_tower_bot, minpoly_eq, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left, isSplittingField_iff, topEquiv_symm_apply_coe, FiniteGaloisIntermediateField.adjoin_val, NumberField.of_intermediateField, rank_top', isAlgebraic_adjoin_simple, AdjoinSimple.normal_algebraicClosure, normal_iff_forall_map_eq', intermediateFieldMap_apply_coe, topEquiv_apply, LinearDisjoint.symm, exists_algHom_adjoin_of_splits', Algebra.normalizedTrace_def, AdjoinSimple.isIntegral_gen, RatFunc.natDegree_num_le_natDegree_minpolyX, exists_lt_finrank_of_infinite_dimensional, adjoin_rank_le_of_isAlgebraic, normal_iInf, Algebra.IsAlgebraic.isNormalClosure_normalClosure, isPurelyInseparable_bot, AlgebraicIndependent.aevalEquivField_apply_coe, LinearDisjoint.exists_field_of_isDomain, isSeparable_adjoin_pair_of_isSeparable, finiteDimensional_left, finiteDimensional_iSup_of_finite, le_perfectClosure_iff, perfectClosure.isAlgebraic, isSeparable_sup, FiniteGaloisIntermediateField.finiteDimensional, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, relfinrank_dvd_finrank_top_of_le, InfiniteGalois.restrictNormalHom_continuous, isAlgebraic_iSup, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, IsGalois.of_separable_splitting_field_aux, coe_equivMap_apply, finrank_le_of_le_left, finInsepDegree_bot, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, krullTopology_mem_nhds_one_iff, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, isSeparable_iSup, krullTopology_mem_nhds_one_iff_of_normal, finrank_bot', isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, separableClosure.isSeparable, RatFunc.isAlgebraic_adjoin_simple_X', Algebra.norm_eq_prod_roots, adjoin.finiteDimensional, botEquiv_def, le_algebraicClosure_iff, adjoin_adjoin_comm, AlgebraicIndependent.algebraicClosure, finSepDegree_bot', val_mk, rank_sup_le, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField, AlgEquiv.restrictNormalHom_apply, InfiniteGalois.mk_toAlgEquivAux, instIsAbelianGaloisSubtypeMemIntermediateField, adjoin_simple_comm, algebraicClosure.isAlgClosure, inclusion_inclusion, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, extendScalars_restrictScalars, mem_extendScalars, perfectClosure.perfectField, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, RatFunc.C_minpolyX, InfiniteGalois.proj_of_le, expChar', exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow, adjoin_minpoly_coeff_of_exists_primitive_element, relrank_eq_rank_of_le, lift_adjoin, extendScalars_top, algebraicIndependent_adjoin_iff, rank_eq_rank_subalgebra, LinearDisjoint.of_finrank_sup, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, lift_sup, normalClosure.normal, adjoin_adjoin_left, normalClosure_mono, AdjoinSimple.coe_aeval_gen_apply, separableClosure_le_iff, LinearDisjoint.basisOfBasisLeft_repr_apply, restrictNormalHom_ker, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin, adjoin_rank_le_of_isAlgebraic_left, algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, insepDegree_bot, equivOfEq_apply, rank_bot', isAlgebraic_adjoin_iff_bot, fieldRange_val, liftAlgEquiv_apply, LinearDisjoint.of_basis_mul, insepDegree_top, separableClosure_le_separableClosure_iff, transcendental_adjoin_iff, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, rank_comap, separableClosure.separableClosure_eq_bot, rank_bot_mul_relrank, instIsInertiaFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupInertiaOfIsGalois, finiteDimensional_map, RatFunc.algEquivOfTranscendental_algebraMap, finSepDegree_top, lift_rank_comap, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_right, instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap, normalClosure_le_iff_of_normal, AlgHom.fieldRange_of_normal, Lifts.eq_iff, IsGaloisGroup.card_fixingSubgroup_eq_finrank, normalClosure_map_eq, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, relrank_bot_left, IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension, IsGaloisGroup.finrank_fixedPoints_eq_card_subgroup, Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, RatFunc.isAlgebraic_adjoin_simple_X, isPurelyInseparable_tower_top, le_normalClosure, equivOfEq_trans, normalClosure_def', Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, mem_restrict, LinearDisjoint.isDomain, finrank_dvd_of_le_right, finrank_le_of_le_right, RatFunc.natDegree_denom_le_natDegree_minpolyX, isGalois_bot, intermediateFieldMap_symm_apply_coe, finrank_dvd_of_le_left, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, isGalois_iff_isGalois_bot, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic, Field.insepDegree_le_of_left_le, finiteDimensional_adjoin_pair, normal_sup, coe_algebraMap_apply, separableClosure.isGalois, isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one, restrictScalars_adjoin, finiteDimensional_iSup_of_finset', finrank_adjoin_simple_eq_one_iff, LinearDisjoint.map, isSeparable_tower_top, RatFunc.algEquivOfTranscendental_apply, normalClosure.is_finiteDimensional, finiteDimensional_sup, Lifts.le_iff, trace_adjoinSimpleGen, normal_iff_normalClosure_eq, rank_adjoin_simple_eq_one_iff, algebraAdjoinAdjoin.coe_algebraMap, isIntegral_iff, LinearDisjoint.isField_of_isAlgebraic, separableClosure.normalClosure_eq_self, adjoin.powerBasis_dim, IsGalois.of_fixedField_normal_subgroup, essFiniteType_iff, Field.Emb.cardinal_separableClosure, isPurelyInseparable_sup, splits_of_splits, separableClosure.isPurelyInseparable, isPurelyInseparable_adjoin_simple_iff_pow_mem, adjoin_rootSet_isSplittingField, nonempty_algHom_adjoin_of_splits, isScalarTower_mid, finSepDegree_bot, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed, LinearDisjoint.linearIndependent_left, perfectClosure.isPurelyInseparable, isSeparable_adjoin_iff_isSeparable, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal, sepDegree_top, extendScalars_le_extendScalars_iff
|
toSubalgebra 📖 | CompOp | 51 mathmath: toSubalgebra_toIntermediateField', algHomEquivAlgHomOfSplits_symm_apply, adjoin_intermediateField_toSubalgebra_of_isAlgebraic, mem_carrier, inf_toSubalgebra, coe_toSubalgebra, Field.Emb.Cardinal.succEquiv_coherence, bot_toSubalgebra, sup_toSubalgebra_of_isAlgebraic_left, AlgHom.fieldRange_toSubalgebra, linearDisjoint_iff, toSubalgebra_map, inv_mem', adjoin_simple_toSubalgebra_of_integral, range_val, sup_toSubalgebra_of_isAlgebraic, linearDisjoint_iff', sInf_toSubalgebra, toIntermediateField'_toSubalgebra, top_toSubalgebra, finrank_eq_finrank_subalgebra, adjoin_eq_algebra_adjoin, toIntermediateField_toSubalgebra, adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left, algebraicClosure_toSubalgebra, adjoin_simple_toSubalgebra_of_isAlgebraic, sup_toSubalgebra_of_left, toSubalgebra_injective, adjoin_toSubalgebra, mem_toSubalgebra, adjoin_toSubalgebra_of_isAlgebraic_right, restrictScalars_toSubalgebra, toSubalgebra_iSup_of_directed, adjoin_toSubalgebra_of_isAlgebraic_left, toSubalgebra_lt_toSubalgebra, isAlgebraic_solvableByRad, coe_type_toSubalgebra, toSubalgebra_inj, rank_eq_rank_subalgebra, toSubalgebra_strictMono, sup_toSubalgebra_of_right, equivOfEq_apply, le_sup_toSubalgebra, adjoin_toSubalgebra_of_isAlgebraic, adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right, sup_toSubalgebra_of_isAlgebraic_right, toSubalgebra_le_toSubalgebra, toSubalgebra_toIntermediateField, iInf_toSubalgebra, adjoin_algebraic_toSubalgebra, algebra_adjoin_le_adjoin
|
toSubfield 📖 | CompOp | 25 mathmath: extendScalars_toSubfield, fieldRange_le, sSup_toSubfield, Subfield.extendScalars_toSubfield, iInf_toSubfield, coe_type_toSubfield, toSubfield_map, mem_toSubfield, Subfield.extendScalars.orderIso_symm_apply, AlgHom.fieldRange_toSubfield, coe_toSubfield, restrictScalars_toSubfield, Subfield.le_extendScalars_iff, Subfield.extendScalars_le_iff, iSup_toSubfield, toSubfield_inj, bot_toSubfield, Subfield.toIntermediateField_toSubfield, top_toSubfield, adjoin_le_subfield, sInf_toSubfield, inf_toSubfield, sup_toSubfield, adjoin_toSubfield, toSubfield_injective
|
val 📖 | CompOp | 11 mathmath: algHomEquivAlgHomOfSplits_apply, exists_algHom_of_adjoin_splits, fieldRange_comp_val, range_val, exists_algHom_of_splits, coe_val, AlgebraicIndependent.liftAlgHom_comp_reprField, LinearDisjoint.linearIndependent_right, val_mk, fieldRange_val, LinearDisjoint.linearIndependent_left
|