adjoin 📖 | CompOp | 235 mathmath: AdjoinSimple.trace_gen_eq_sum_roots, aeval_gen_minpoly, adjoin_eq_top_iff_of_isAlgebraic, adjoin.finrank, adjoin_intermediateField_toSubalgebra_of_isAlgebraic, adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable', minpoly.algEquiv_apply, adjoinRootEquivAdjoin_symm_apply_gen, isCyclotomicExtension_singleton_iff_eq_adjoin, Field.Emb.Cardinal.filtration_succ, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_right, mem_adjoin_iff, Field.exists_primitive_element, adjoin_eq_adjoin_pow_expChar_of_isSeparable, adjoin_simple_isCompactElement, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic, adjoin.mono, Algebra.FormallySmooth.adjoin_of_algebraicIndependent, algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, adjoin_zero, PowerBasis.equivAdjoinSimple_symm_aeval, adjoin_univ, lift_adjoin_simple, AdjoinDouble.normal_algebraicClosure, mem_adjoin_simple_self, adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable, isAlgebraic_adjoin_iff_top, adjoin_finite_isCompactElement, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', mem_adjoin_of_mem, subset_adjoin_of_subset_left, adjoin_le_iff, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, IsNormalClosure.adjoin_rootSet, Field.Emb.Cardinal.two_le_deg, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic, IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq, isAlgebraic_adjoin_iff, minpoly_gen, Field.Emb.Cardinal.isLeast_leastExt, normalClosure_eq_iSup_adjoin', Field.Emb.Cardinal.succEquiv_coherence, finSepDegree_adjoin_simple_eq_finrank_iff, fg_adjoin_finset, Field.primitive_element_iff_algHom_eq_of_eval', adjoin.powerBasis_gen, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, adjoin_simple_toSubalgebra_of_integral, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right, mem_adjoin_pair_right, AdjoinSimple.norm_gen_eq_one, restrictScalars_adjoin_of_algEquiv, adjoin_map, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, IsFractionRing.algHom_fieldRange_eq_of_comp_eq, AlgebraicIndependent.lift_reprField, isAlgebraic_adjoin, sSup_def, IsTranscendenceBasis.isAlgebraic_field, PowerBasis.equivAdjoinSimple_aeval, Field.exists_primitive_element_of_finite_bot, Field.exists_primitive_element_of_finite_top, instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap, adjoin_simple_eq_top_iff_of_isAlgebraic, trace_eq_finrank_mul_minpoly_nextCoeff, rank_adjoin_eq_one_iff, adjoin_one, trace_eq_trace_adjoin, adjoin_root_eq_top, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, exists_finset_of_mem_supr'', adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable, PowerBasis.equivAdjoinSimple_gen, restrictScalars_adjoin_eq_sup, mem_adjoin_iff_div, cardinalMk_adjoin_le, fg_def, PowerBasis.equivAdjoinSimple_symm_gen, exists_root_adjoin_eq_top_of_isCyclic, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable', NumberField.is_primitive_element_of_infinitePlace_lt, IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq, finrank_adjoin_eq_one_iff, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow_of_essFiniteType, subset_adjoin_of_subset_right, trace_eq_sum_roots, adjoin_simple_le_iff, Algebra.norm_eq_norm_adjoin, subset_adjoin, isAlgebraic_adjoin_iff_isAlgebraic, adjoin.range_algebraMap_subset, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable, sup_def, isAlgebraic_adjoin_pair, adjoin_empty, adjoinRootEquivAdjoin_apply_root, adjoin_eq_algebra_adjoin, finSepDegree_adjoin_simple_eq_natSepDegree, isPurelyInseparable_adjoin_iff_pow_mem, separableClosure.adjoin_eq_of_isAlgebraic, adjoin.algebraMap_mem, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right, finiteDimensional_adjoin, isTranscendenceBasis_adjoin_iff, adjoin_intermediateField_toSubalgebra_of_isAlgebraic_left, adjoin_eq_bot_iff, isSeparable_adjoin_simple_iff_isSeparable, AdjoinSimple.trace_gen_eq_zero, mem_adjoin_range_iff, finSepDegree_adjoin_simple_le_finrank, Field.exists_primitive_element_iff_finite_intermediateField, card_algHom_adjoin_integral, Field.Emb.Cardinal.filtration_apply, AdjoinPair.algebraMap_gen₁, adjoin_simple_toSubalgebra_of_isAlgebraic, AlgebraicIndependent.liftAlgHom_comp_reprField, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, Field.Emb.Cardinal.deg_lt_aleph0, algHomAdjoinIntegralEquiv_symm_apply_gen, adjoin_simple_eq_bot_iff, iSup_eq_adjoin, adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable', exists_isTranscendenceBasis_and_isSeparable_of_perfectField, fg_adjoin_of_finite, adjoin_intCast, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic_left, Field.primitive_element_iff_minpoly_degree_eq, adjoin_toSubalgebra, adjoin_rank_le_of_isAlgebraic_right, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_left, mem_adjoin_pair_left, algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, adjoin_root_eq_top_of_isSplittingField, adjoin_iUnion, algebraicClosure.adjoin_le, adjoin_simple_eq_adjoin_pow_expChar_of_isSeparable', Field.primitive_element_iff_minpoly_natDegree_eq, AdjoinSimple.norm_gen_eq_prod_roots, Field.Emb.Cardinal.strictMono_filtration, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left, isSplittingField_iff, FiniteGaloisIntermediateField.adjoin_val, adjoin_finset_isCompactElement, adjoin_eq_range_algebraMap_adjoin, isAlgebraic_adjoin_simple, exists_finset_of_mem_supr', AdjoinSimple.normal_algebraicClosure, exists_algHom_adjoin_of_splits', Algebra.normalizedTrace_def, adjoin_natCast, AdjoinSimple.isIntegral_gen, adjoin_rank_le_of_isAlgebraic, AlgebraicIndependent.aevalEquivField_apply_coe, adjoin_toSubalgebra_of_isAlgebraic_right, isSeparable_adjoin_pair_of_isSeparable, normalClosure_eq_iSup_adjoin, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left, IsGalois.of_separable_splitting_field_aux, adjoin_le_subfield, adjoin_insert_adjoin, mem_adjoin_simple_iff, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, Field.Emb.Cardinal.iSup_adjoin_eq_top, lift_cardinalMk_adjoin_le, isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, adjoin_toSubalgebra_of_isAlgebraic_left, Algebra.norm_eq_prod_roots, adjoin.finiteDimensional, adjoin_adjoin_comm, adjoin_eq_top_iff, adjoin_simple_comm, Field.Emb.Cardinal.adjoin_image_leastExt, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic, adjoin_subset_adjoin_iff, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow, adjoin_union, Field.exists_primitive_element_of_finite_intermediateField, lift_adjoin, adjoin_eq_top_of_algebra, algebraicIndependent_adjoin_iff, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, adjoin_adjoin_left, IsFractionRing.liftAlgHom_fieldRange, adjoin_rank_le_of_isAlgebraic_left, algebraAdjoinAdjoin.instFaithfulSMulSubtypeMemSubalgebraAdjoinAdjoin, gc, isAlgebraic_adjoin_iff_bot, adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable, transcendental_adjoin_iff, adjoin_toSubalgebra_of_isAlgebraic, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, adjoin_intermediateField_toSubalgebra_of_isAlgebraic_right, adjoin_toSubfield, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_right, IsAdjoinRoot.primitive_element_root, instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetAdjoinCoeRingHomAlgebraMap, Field.Emb.Cardinal.adjoin_basis_eq_top, adjoin_eq_adjoin_pow_expChar_of_isSeparable', LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension, adjoin_self, adjoin_algebraic_toSubalgebra, AdjoinSimple.coe_gen, isSplittingField_iff_intermediateField, eq_adjoin_of_eq_algebra_adjoin, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits, LinearDisjoint.adjoin_rank_eq_rank_right_of_isAlgebraic, finiteDimensional_adjoin_pair, isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one, restrictScalars_adjoin, finrank_adjoin_simple_eq_one_iff, Field.primitive_element_iff_algHom_eq_of_eval, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin, trace_adjoinSimpleGen, rank_adjoin_simple_eq_one_iff, separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable, AdjoinPair.algebraMap_gen₂, adjoin.powerBasis_dim, AdjoinSimple.algebraMap_gen, separableClosure.adjoin_le, algebra_adjoin_le_adjoin, isPurelyInseparable_adjoin_simple_iff_pow_mem, isCyclic_tfae, adjoin_rootSet_isSplittingField, nonempty_algHom_adjoin_of_splits, biSup_adjoin_simple, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed, isSeparable_adjoin_iff_isSeparable, Field.primitive_element_inf_aux, adjoin_contains_field_as_subfield
|
instCompleteLattice 📖 | CompOp | 242 mathmath: finInsepDegree_top, adjoin_eq_top_iff_of_isAlgebraic, LinearDisjoint.iff_inf_eq_bot, normal_inf, sSup_toSubfield, extendScalars_sup, coe_algebraMap_over_bot, relrank_comap_comap_eq_relrank_inf, isPurelyInseparable_iSup, coe_bot, lift_insepDegree_bot', algebraicClosure.algebraicClosure_eq_bot, coe_iSup_of_directed, IsGaloisGroup.fixingSubgroup_top, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax, IsGaloisGroup.fixedPoints_top, botEquiv_symm, AlgHom.fieldRange_eq_map, relfinrank_bot_right, Field.exists_primitive_element, isGalois_iff_isGalois_top, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, InfiniteGalois.mem_bot_iff_fixed, adjoin_zero, coe_iInf, adjoin_univ, inf_toSubalgebra, finiteDimensional_iSup_of_finset, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isComplex, IsNormalClosure.adjoin_rootSet, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, inf_relrank_right, normalClosure_eq_iSup_adjoin', iInf_toSubfield, fixingSubgroup_top, bot_toSubalgebra, sup_toSubalgebra_of_isAlgebraic_left, relfinrank_top_right, restrictScalars_sup, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, restrictScalars_top, mem_top, Field.primitive_element_iff_algHom_eq_of_eval', Subfield.extendScalars_inf, relrank_top_right, LinearDisjoint.bot_left, isTotallyReal_bot, normal_iSup, instFiniteSubtypeMemBot, isCyclotomicExtension_lcm_sup, sup_toSubalgebra_of_isAlgebraic, finrank_eq_one_iff, lift_top, sInf_toSubalgebra, eq_bot_of_isAlgClosed_of_isAlgebraic, insepDegree_bot', fg_sup, inf_relfinrank_right, sSup_def, restrictScalars_eq_top_iff, bot_eq_top_of_finrank_adjoin_eq_one, extendScalars_inf, botContinuousSMul, Field.exists_primitive_element_of_finite_bot, Field.exists_primitive_element_of_finite_top, adjoin_simple_eq_top_iff_of_isAlgebraic, rank_adjoin_eq_one_iff, adjoin_one, rank_top, adjoin_root_eq_top, normalClosure_def, lift_inf, instIsCompactlyGenerated, extendScalars_self, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin_1, coe_inf, finrank_top, restrictScalars_adjoin_eq_sup, separableClosure.eq_top_iff, mem_inf, top_toSubalgebra, relrank_top_left, IsGaloisGroup.fixedPoints_bot, exists_root_adjoin_eq_top_of_isCyclic, finrank_eq_one_iff_eq_top, Subfield.extendScalars_top, LinearDisjoint.finrank_sup, NumberField.is_primitive_element_of_infinitePlace_lt, finrank_adjoin_eq_one_iff, bot_eq_top_of_rank_adjoin_eq_one, restrictScalars_inf, finrank_bot, InfiniteGalois.restrict_fixedField, sepDegree_bot, finInsepDegree_bot', restrictScalars_bot_eq_self, fg_bot, sup_def, finrank_sup_le, adjoin_empty, Field.Emb.Cardinal.eq_bot_of_not_nonempty, rank_bot, separableClosure_inf_perfectClosure, bot_eq_top_iff_finrank_eq_one, adjoin_eq_bot_iff, lift_sepDegree_bot', relfinrank_inf_mul_relfinrank, LinearDisjoint.inf_eq_bot, Field.exists_primitive_element_iff_finite_intermediateField, Field.Emb.Cardinal.filtration_apply, map_comap_eq, map_iSup, map_iInf, finrank_top', lift_bot, NumberField.mixedEmbedding.exists_primitive_element_lt_of_isReal, IsGalois.fixedField_top, Algebra.IsAlgebraic.isNormalClosure_iff, sup_toSubalgebra_of_left, isSplittingField_iSup, adjoin_simple_eq_bot_iff, relfinrank_bot_left, iSup_eq_adjoin, LinearDisjoint.rank_sup, rank_sup_le_of_isAlgebraic, adjoin_intCast, iSup_toSubfield, sepDegree_bot', LinearDisjoint.bot_right, Field.primitive_element_iff_minpoly_degree_eq, AlgHom.fieldRange_eq_top, isPurelyInseparable_iff_perfectClosure_eq_top, rank_eq_one_iff, relfinrank_mul_relfinrank_eq_inf_relfinrank, fg_iSup, eq_bot_of_isPurelyInseparable_of_isSeparable, adjoin_root_eq_top_of_isSplittingField, algebraicClosure.eq_top_iff, adjoin_iUnion, Field.primitive_element_iff_minpoly_natDegree_eq, normalClosure_def'', isScalarTower_over_bot, relfinrank_inf_mul_relfinrank_of_le, bot_toSubfield, topEquiv_symm_apply_coe, relrank_inf_mul_relrank_of_le, rank_top', topEquiv_apply, adjoin_natCast, normal_iInf, isPurelyInseparable_bot, top_toSubfield, Subfield.extendScalars_sup, finiteDimensional_iSup_of_finite, isSeparable_sup, IsGaloisGroup.fixingSubgroup_bot, isAlgebraic_iSup, normalClosure_eq_iSup_adjoin, fg_top, finInsepDegree_bot, AlgEquiv.fieldRange_eq_top, Field.Emb.Cardinal.iSup_adjoin_eq_top, toSubalgebra_iSup_of_directed, isSeparable_iSup, finrank_bot', sInf_toSubfield, botEquiv_def, adjoin_eq_top_iff, finSepDegree_bot', rank_sup_le, eq_bot_of_isSepClosed_of_isSeparable, bot_eq_top_of_finrank_adjoin_le_one, relrank_bot_right, InfiniteGalois.fixedField_bot, IsSepClosed.separableClosure_eq_bot_iff, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin, lift_relrank_comap_comap_eq_lift_relrank_inf, adjoin_union, inf_toSubfield, adjoin_eq_top_of_algebra, extendScalars_top, perfectClosure.eq_bot_of_isSeparable, fixedField_bot, lift_sup, FiniteGaloisIntermediateField.instIsSeparableSubtypeMemIntermediateFieldMin, sup_toSubalgebra_of_right, insepDegree_bot, IsAlgClosed.algebraicClosure_eq_bot_iff, rank_bot', le_sup_toSubalgebra, insepDegree_top, IsGalois.tfae, map_inf, Field.Emb.Cardinal.iSup_filtration, isSimpleOrder_of_finrank_prime, LinearDisjoint.eq_bot_of_self, separableClosure.separableClosure_eq_bot, fg_top_iff, sup_toSubfield, relfinrank_comap_comap_eq_relfinrank_inf, sup_toSubalgebra_of_isAlgebraic_right, inf_relfinrank_left, relfinrank_top_left, map_sup, finSepDegree_top, inf_relrank_left, IsAdjoinRoot.primitive_element_root, Subfield.extendScalars_self, Field.Emb.Cardinal.adjoin_basis_eq_top, relrank_inf_mul_relrank, iInf_toSubalgebra, relrank_bot_left, Lifts.carrier_union, normalClosure_def', mem_bot, relrank_mul_relrank_eq_inf_relrank, fixingSubgroup_bot, coe_top, isGalois_bot, coe_sInf, isSplittingField_iff_intermediateField, isGalois_iff_isGalois_bot, Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits, normal_sup, finiteDimensional_iSup_of_finset', finrank_adjoin_simple_eq_one_iff, Field.primitive_element_iff_algHom_eq_of_eval, finiteDimensional_sup, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin, separableClosure.eq_bot_iff, fixingSubgroup_sup, rank_adjoin_simple_eq_one_iff, separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable, isPurelyInseparable_sup, IsGalois.mem_bot_iff_fixed, map_bot, isCyclic_tfae, separableClosure.eq_bot_of_isPurelyInseparable, finSepDegree_bot, biSup_adjoin_simple, sepDegree_top, IsGaloisGroup.fixedPoints_eq_bot
|