Basic

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

Statistics

Metric	Count
Definitions fieldRange, inhabited, algebra', comap, copy, equivMap, equivOfEq, extendScalars, orderIso, inclusion, instAlgebraSubtypeMem, instAlgebraSubtypeMem_1, instDistribMulActionSubtypeMem, instModuleSubtypeMem, instModuleSubtypeMem_1, instMulActionSubtypeMem, instMulActionWithZeroSubtypeMem, instMulDistribMulActionSubtypeMem, instMulSemiringActionSubtypeMem, instPartialOrder, instSMulSubtypeMem, instSMulSubtypeMem_1, instSMulWithZeroSubtypeMem, instSetLike, intermediateFieldMap, liftAlgEquiv, map, module', restrict, restrictScalars, restrict_algEquiv, toAlgebra, toField, toSubalgebra, toSubfield, val, toIntermediateField, toIntermediateField', extendScalars, orderIso, toIntermediateField	41
Theorems coe_fieldRange, fieldRange_toSubalgebra, fieldRange_toSubfield, mem_fieldRange, add_mem, aeval_coe, algebraMap_apply, algebraMap_mem, coe_add, coe_algebraMap_apply, coe_copy, coe_equivMap_apply, coe_extendScalars, coe_inclusion, coe_inv, coe_map, coe_mul, coe_neg, coe_one, coe_pow, coe_prod, coe_restrictScalars, coe_smul, coe_sum, coe_toSubalgebra, coe_toSubfield, coe_type_toSubalgebra, coe_type_toSubfield, coe_val, coe_zero, copy_eq, div_mem, equivOfEq_apply, equivOfEq_rfl, equivOfEq_symm, equivOfEq_trans, ext, ext_iff, orderIso_apply, orderIso_symm_apply_coe, extendScalars_injective, extendScalars_le_extendScalars_iff, extendScalars_le_iff, extendScalars_restrictScalars, extendScalars_toSubfield, fieldRange_comp_val, fieldRange_le, fieldRange_val, gc_map_comap, inclusion_inclusion, inclusion_injective, inclusion_self, instFaithfulSMulSubtypeMem, instIsScalarTowerSubtypeMem, instIsScalarTowerSubtypeMem_1, instSMulMemClass, instSubfieldClass, intCast_mem, intermediateFieldMap_apply_coe, intermediateFieldMap_symm_apply_coe, inv_mem, inv_mem', isScalarTower, isScalarTower_bot, isScalarTower_mid, isScalarTower_mid', le_extendScalars_iff, liftAlgEquiv_apply, lift_inj, lift_injective, lift_le, lift_restrict, list_prod_mem, list_sum_mem, map_id, map_injective, map_le_iff_le_comap, map_map, map_mono, mem_carrier, mem_extendScalars, mem_lift, mem_mk, mem_restrict, mem_restrictScalars, mem_toSubalgebra, mem_toSubfield, mul_mem, multiset_prod_mem, multiset_sum_mem, natCast_mem, neg_mem, one_mem, pow_mem, prod_mem, range_val, restrictScalars_inj, restrictScalars_injective, restrictScalars_toSubalgebra, restrictScalars_toSubfield, set_range_subset, smulCommClass_left, smulCommClass_right, smul_def, smul_mem, sub_mem, sum_mem, toSubalgebra_inj, toSubalgebra_injective, toSubalgebra_le_toSubalgebra, toSubalgebra_lt_toSubalgebra, toSubalgebra_map, toSubalgebra_strictMono, toSubfield_inj, toSubfield_injective, toSubfield_map, val_mk, zero_mem, zsmul_mem, coe_extendScalars, coe_toIntermediateField, orderIso_apply, orderIso_symm_apply_coe, extendScalars_injective, extendScalars_le_extendScalars_iff, extendScalars_le_iff, extendScalars_toSubfield, le_extendScalars_iff, mem_extendScalars, toIntermediateField_toSubfield, toIntermediateField'_toSubalgebra, toIntermediateField_toSubalgebra, toSubalgebra_toIntermediateField, toSubalgebra_toIntermediateField'	134
Total	175

AlgHom

Definitions

Name	Category	Theorems
fieldRange 📖	CompOp	31 math math: normalClosure_le_iff, IntermediateField.relrank_comap_comap_eq_relrank_inf, fieldRange_eq_map, IntermediateField.LinearDisjoint.of_isField', IsFractionRing.algHom_fieldRange_eq_of_comp_eq_of_range_eq, fieldRange_toSubalgebra, IntermediateField.fieldRange_comp_val, normalClosure.restrictScalars_eq, IsFractionRing.algHom_fieldRange_eq_of_comp_eq, IntermediateField.normal_iff_forall_fieldRange_le, normalClosure_def, IntermediateField.linearDisjoint_comm', map_fieldRange, fieldRange_toSubfield, IsFractionRing.liftAlgHom_fieldRange_eq_of_range_eq, IntermediateField.normal_iff_forall_fieldRange_eq, IntermediateField.map_comap_eq, coe_fieldRange, fieldRange_eq_top, mem_fieldRange, IntermediateField.finrank_comap, IntermediateField.LinearDisjoint.exists_field_of_isDomain, fieldRange_le_normalClosure, AlgEquiv.fieldRange_eq_top, IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf, IsFractionRing.liftAlgHom_fieldRange, IntermediateField.fieldRange_val, IntermediateField.rank_comap, IntermediateField.relfinrank_comap_comap_eq_relfinrank_inf, IntermediateField.lift_rank_comap, fieldRange_of_normal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_fieldRange 📖	mathematical	—	SetLike.coe IntermediateField IntermediateField.instSetLike fieldRange Set.range DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring funLike	—	—
fieldRange_toSubalgebra 📖	mathematical	—	IntermediateField.toSubalgebra fieldRange range Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	—
fieldRange_toSubfield 📖	mathematical	—	IntermediateField.toSubfield fieldRange RingHom.fieldRange Field.toDivisionRing RingHomClass.toRingHom AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass algHomClass	—	—
mem_fieldRange 📖	mathematical	—	IntermediateField SetLike.instMembership IntermediateField.instSetLike fieldRange DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring funLike	—	—

IntermediateField

Definitions

Name	Category	Theorems
algebra' 📖	CompOp	244 math math: 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, coe_algebraMap_over_bot, instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic, minpoly.algEquiv_apply, isScalarTower_mid', adjoinRootEquivAdjoin_symm_apply_gen, isCyclotomicExtension_singleton_iff_eq_adjoin, 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, 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, coe_inclusion, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, minpoly_gen, aeval_coe, Field.Emb.Cardinal.succEquiv_coherence, finSepDegree_adjoin_simple_eq_finrank_iff, solvableByRad.isSolvable, linearDisjoint_comm, Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, equivOfEq_symm, restrictRestrictAlgEquivMapHom_apply, fieldRange_comp_val, adjoin.powerBasis_gen, equivOfEq_rfl, normal_iff_normalClosure_le, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, restrictRestrictAlgEquivMapHom_surjective, 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, PowerBasis.equivAdjoinSimple_aeval, isPurelyInseparable_tower_bot, le_separableClosure_iff, botContinuousSMul, eq_separableClosure_iff, normal_iff_forall_fieldRange_le, IsGalois.normalAutEquivQuotient_apply, trace_eq_trace_adjoin, coe_isIntegral_iff, InfiniteGalois.proj_adjoin_singleton_val, lift_inf, 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', Algebra.norm_eq_norm_adjoin, isAlgebraic_adjoin_iff_isAlgebraic, 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, lift_injective, isSeparable_adjoin_simple_iff_isSeparable, AdjoinSimple.trace_gen_eq_zero, lift_sepDegree_bot', 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, 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, spectralNorm.eq_of_normalClosure', separableClosure.isSepClosure, InfiniteGalois.toAlgEquivAux_eq_liftNormal, normalClosure_def'', 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, exists_algHom_adjoin_of_splits', Algebra.normalizedTrace_def, AdjoinSimple.isIntegral_gen, 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, IsGalois.of_separable_splitting_field_aux, coe_equivMap_apply, finInsepDegree_bot, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot, 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, InfiniteGalois.proj_of_le, lift_adjoin, LinearDisjoint.of_finrank_sup, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, lift_sup, normalClosure.normal, adjoin_adjoin_left, normalClosure_mono, solvableByRad.isIntegral, 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, 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, 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, Lifts.le_iff, trace_adjoinSimpleGen, normal_iff_normalClosure_eq, isIntegral_iff, 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 math math: 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 math math: copy_eq, coe_copy
equivMap 📖	CompOp	1 math math: coe_equivMap_apply
equivOfEq 📖	CompOp	4 math math: equivOfEq_symm, equivOfEq_rfl, equivOfEq_apply, equivOfEq_trans
extendScalars 📖	CompOp	22 math math: 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	8 math math: exists_algHom_adjoin_of_splits, coe_inclusion, Lifts.lt_iff, inclusion_self, inclusion_injective, inclusion_inclusion, Lifts.eq_iff, Lifts.le_iff
instAlgebraSubtypeMem 📖	CompOp	103 math math: 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, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, extendScalars_injective, LinearDisjoint.of_isField', isAlgebraic_adjoin_iff_top, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', Field.Emb.Cardinal.two_le_deg, finInsepDegree_le_of_left_le, isAlgebraic_adjoin_iff, Field.Emb.Cardinal.succEquiv_coherence, linearDisjoint_comm, restrictRestrictAlgEquivMapHom_apply, IsGalois.sup_right, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, normalClosure.restrictScalars_eq, restrictRestrictAlgEquivMapHom_surjective, linearDisjoint_iff', extendScalars.orderIso_apply, algebraicClosure.isIntegralClosure, Field.Emb.Cardinal.instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, IsTranscendenceBasis.isAlgebraic_field, extendScalars_adjoin, extendScalars_inf, botContinuousSMul, eq_separableClosure_iff, IsGalois.normalAutEquivQuotient_apply, isAlgebraic_tower_top, 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, restrictScalars_bot_eq_self, Differential.instDifferentialAlgebraSubtypeMemIntermediateField_1, le_restrictScalars_separableClosure, instIsScalarTowerSubtypeMem_1, 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, 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, relfinrank_eq_finrank_of_le, adjoin_eq_range_algebraMap_adjoin, LinearDisjoint.exists_field_of_isDomain, InfiniteGalois.restrictNormalHom_continuous, IsGaloisGroup.subgroup, 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, restrictNormalHom_ker, LinearDisjoint.of_basis_mul, separableClosure_le_separableClosure_iff, transcendental_adjoin_iff, separableClosure.separableClosure_eq_bot, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_left, 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, isSeparable_tower_top, AdjoinPair.algebraMap_gen₂, AdjoinSimple.algebraMap_gen, separableClosure.isPurelyInseparable, extendScalars_le_extendScalars_iff
instAlgebraSubtypeMem_1 📖	CompOp	4 math math: 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	42 math math: 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, 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 math math: 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	90 math math: normalClosure_le_iff, Field.Emb.Cardinal.equivLim_coherence, 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, 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, Field.Emb.Cardinal.equivSucc_coherence, le_algebraicClosure, Lifts.lt_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, Subfield.extendScalars_le_iff, extendScalars.orderIso_symm_apply_coe, 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, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, le_algebraicClosure_iff, toSubalgebra_lt_toSubalgebra, fixedField_le, le_iff_le, IsGaloisGroup.fixedPoints_le_of_le, extendScalars_top, le_separableClosure', toSubalgebra_strictMono, separableClosure_le_iff, isClosed_restrictScalars_separableClosure, gc, FiniteGaloisIntermediateField.le_iff, separableClosure_le_separableClosure_iff, Field.Emb.Cardinal.iSup_filtration, isSimpleOrder_of_finrank_prime, Subfield.extendScalars.orderIso_symm_apply_coe, le_separableClosure, toSubalgebra_le_toSubalgebra, normalClosure_le_iff_of_normal, Lifts.eq_iff, le_normalClosure, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, 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
instSMulSubtypeMem 📖	CompOp	15 math math: 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 math math: instIsScalarTowerSubtypeMem_1
instSMulWithZeroSubtypeMem 📖	CompOp	—
instSetLike 📖	CompOp	513 math math: 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, IsGalois.tower_top_intermediateField, LinearDisjoint.linearIndependent_right', adjoin.finrank, algebraMap_mem, extendScalars_sup, coe_algebraMap_over_bot, instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic, mem_subalgebraEquivIntermediateField, minpoly.algEquiv_apply, isScalarTower_mid', adjoinRootEquivAdjoin_symm_apply_gen, isCyclotomicExtension_singleton_iff_eq_adjoin, 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, botEquiv_symm, relrank_mul_rank_top, IsGalois.card_fixingSubgroup_eq_finrank, Subfield.relfinrank_eq_finrank_of_le, isGalois_iff_isGalois_top, 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, coe_neg, restrictScalars_normal, isScalarTower, Algebra.FormallySmooth.adjoin_of_algebraicIndependent, algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin, isPurelyInseparable_iff_fd_isPurelyInseparable, LinearDisjoint.of_isField', coe_iInf, PowerBasis.equivAdjoinSimple_symm_aeval, Subfield.coe_toIntermediateField, lift_adjoin_simple, algebraicClosure.normalClosure_eq_self, AdjoinDouble.normal_algebraicClosure, coe_add, mem_adjoin_simple_self, isAlgebraic_adjoin_iff_top, algebraicClosure.isAlgebraic, IsGalois.normalClosure, exists_isTranscendenceBasis_and_isSeparable_of_linearIndepOn_pow', finiteDimensional_right, isAlgebraic_iff, charZero, NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic, mem_adjoin_of_mem, subset_adjoin_of_subset_left, instSMulMemClass, coe_inclusion, adjoin_le_iff, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, Field.Emb.Cardinal.two_le_deg, smulCommClass_left, finInsepDegree_le_of_left_le, isAlgebraic_adjoin_iff, minpoly_gen, Field.Emb.Cardinal.isLeast_leastExt, aeval_coe, instIsScalarTowerSubtypeMem, coe_toSubalgebra, Field.Emb.Cardinal.succEquiv_coherence, isScalarTower_bot, relfinrank_top_right, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, finSepDegree_adjoin_simple_eq_finrank_iff, solvableByRad.isSolvable, linearDisjoint_comm, 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, relfinrank_dvd_finrank_bot, IsGalois.sup_right, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, normalClosure.restrictScalars_eq, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right, mem_adjoin_pair_right, restrictRestrictAlgEquivMapHom_surjective, AdjoinSimple.norm_gen_eq_one, range_val, instFiniteSubtypeMemBot, isCyclotomicExtension_lcm_sup, map_mem_perfectClosure_iff, linearDisjoint_iff', IsGaloisGroup.fixedPoints_fixingSubgroup, splits_iff_mem, extendScalars.orderIso_apply, algebraicClosure.isIntegralClosure, Algebra.normalizedTrace_intermediateField, 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', AlgebraicIndependent.lift_reprField, isAlgebraic_adjoin, mem_subalgebraEquivIntermediateField_symm, instIsLiouvilleSubtypeMemIntermediateField, coe_mul, sSup_def, IsTranscendenceBasis.isAlgebraic_field, Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, PowerBasis.equivAdjoinSimple_aeval, extendScalars_adjoin, isPurelyInseparable_tower_bot, le_separableClosure_iff, charP', toIntermediateField'_toSubalgebra, extendScalars_inf, botContinuousSMul, eq_separableClosure_iff, mem_toSubfield, mem_algebraicClosure_iff, normal_iff_forall_fieldRange_le, IsGalois.normalAutEquivQuotient_apply, instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap, 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, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, IsGaloisGroup.fixingSubgroup_fixedPoints, lift_inf, mem_perfectClosure_iff, 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, Lifts.lt_iff, mem_inf, extendScalars_le_iff, instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, cardinalMk_adjoin_le, coe_sum, Splits.algebraicClosure, PowerBasis.equivAdjoinSimple_symm_gen, coe_val, IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply, finrank_eq_finrank_subalgebra, finrank_eq_one_iff_eq_top, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable', restrictRestrictAlgEquivMapHom_injective, Transcendental.algebraicClosure, coe_toSubfield, 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, subset_adjoin_of_subset_right, sepDegree_bot, normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure, trace_eq_sum_roots, algebraMap_apply, adjoin_simple_le_iff, finInsepDegree_bot', Algebra.norm_eq_norm_adjoin, subset_adjoin, isAlgebraic_adjoin_iff_isAlgebraic, 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, 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, finrank_bot_mul_relfinrank, 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, 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, finSepDegree_adjoin_simple_le_finrank, card_algHom_adjoin_integral, relrank_dvd_rank_bot, AdjoinPair.algebraMap_gen₁, 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, InfiniteGalois.isOpen_iff_finite, Field.Emb.Cardinal.deg_lt_aleph0, algHomAdjoinIntegralEquiv_symm_apply_gen, adjoin_simple_eq_bot_iff, relfinrank_bot_left, iSup_eq_adjoin, le_extendScalars_iff, 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, IsGaloisGroup.intermediateField, adjoin_rank_le_of_isAlgebraic_right, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic_left, 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, normalClosure_def'', 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, 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, rank_top', isAlgebraic_adjoin_simple, AdjoinSimple.normal_algebraicClosure, normal_iff_forall_map_eq', intermediateFieldMap_apply_coe, topEquiv_apply, exists_algHom_adjoin_of_splits', Algebra.normalizedTrace_def, coe_inv, AdjoinSimple.isIntegral_gen, map_mem_algebraicClosure_iff, mem_restrictScalars, exists_lt_finrank_of_infinite_dimensional, Algebra.IsAlgebraic.isNormalClosure_normalClosure, 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, le_perfectClosure_iff, perfectClosure.isAlgebraic, isSeparable_sup, FiniteGaloisIntermediateField.finiteDimensional, 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, 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, IsGaloisGroup.intermediateFieldEquivSubgroup_apply, krullTopology_mem_nhds_one_iff, one_mem, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, lift_cardinalMk_adjoin_le, krullTopology_mem_nhds_one_iff_of_normal, finrank_bot', isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, Lifts.exists_lift_of_splits, separableClosure.isSeparable, adjoin_toSubalgebra_of_isAlgebraic_left, Algebra.norm_eq_prod_roots, adjoin.finiteDimensional, botEquiv_def, le_algebraicClosure_iff, adjoin_adjoin_comm, AlgebraicIndependent.algebraicClosure, finSepDegree_bot', rank_sup_le, coe_pow, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField, AlgEquiv.restrictNormalHom_apply, instIsAbelianGaloisSubtypeMemIntermediateField, adjoin_simple_comm, algebraicClosure.isAlgClosure, inclusion_inclusion, extendScalars_restrictScalars, zero_mem, adjoin_subset_adjoin_iff, mem_extendScalars, perfectClosure.perfectField, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, mem_mk, 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, smulCommClass_right, extendScalars_top, algebraicIndependent_adjoin_iff, mem_separableClosure_iff, rank_eq_rank_subalgebra, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, lift_sup, normalClosure.normal, adjoin_adjoin_left, normalClosure_mono, separableClosure_le_iff, solvableByRad.isIntegral, 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, 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, finiteDimensional_map, 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, isPurelyInseparable_tower_top, le_normalClosure, equivOfEq_trans, 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, 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, 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, finrank_adjoin_simple_eq_one_iff, isSeparable_tower_top, normalClosure.is_finiteDimensional, finiteDimensional_sup, Lifts.le_iff, trace_adjoinSimpleGen, normal_iff_normalClosure_eq, rank_adjoin_simple_eq_one_iff, separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable, AdjoinPair.algebraMap_gen₂, isIntegral_iff, 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, separableClosure.adjoin_le, IsGalois.mem_bot_iff_fixed, FiniteGaloisIntermediateField.adjoin_simple_le_iff, 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, 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 math math: intermediateFieldMap_apply_coe, intermediateFieldMap_symm_apply_coe
liftAlgEquiv 📖	CompOp	1 math math: liftAlgEquiv_apply
map 📖	CompOp	52 math math: 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, 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, normalClosure_def', intermediateFieldMap_symm_apply_coe, map_id, LinearDisjoint.map, comap_map, coe_map, map_bot
module' 📖	CompOp	70 math math: adjoin.finrank, InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, Subfield.relfinrank_eq_finrank_of_le, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, LinearDisjoint.adjoin_rank_eq_rank_left_of_isAlgebraic, isScalarTower, LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, 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, 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, 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 math math: mem_restrict, lift_restrict
restrictScalars 📖	CompOp	42 math math: 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 math math: algebraMap_apply
toField 📖	CompOp	395 math math: 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, IsGalois.tower_top_intermediateField, LinearDisjoint.linearIndependent_right', adjoin.finrank, extendScalars_sup, coe_algebraMap_over_bot, instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic, SeparableClosure.isSepClosed, minpoly.algEquiv_apply, isScalarTower_mid', adjoinRootEquivAdjoin_symm_apply_gen, isCyclotomicExtension_singleton_iff_eq_adjoin, 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, botEquiv_symm, relrank_mul_rank_top, IsGalois.card_fixingSubgroup_eq_finrank, Subfield.relfinrank_eq_finrank_of_le, isGalois_iff_isGalois_top, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, exists_algHom_of_adjoin_splits, normal_iff_forall_map_eq, extendScalars_injective, restrictScalars_normal, isScalarTower, 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, charZero, NumberField.instIsTotallyRealSubtypeMemIntermediateFieldRatOfIsAlgebraic, coe_inclusion, instIsAbelianGaloisSubtypeMemIntermediateFieldBot, Field.Emb.Cardinal.two_le_deg, finInsepDegree_le_of_left_le, isAlgebraic_adjoin_iff, minpoly_gen, aeval_coe, Field.Emb.Cardinal.succEquiv_coherence, relfinrank_top_right, FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin, finSepDegree_adjoin_simple_eq_finrank_iff, solvableByRad.isSolvable, 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, relfinrank_dvd_finrank_bot, IsGalois.sup_right, exists_finset_maximalFor_isTranscendenceBasis_separableClosure, adjoin_simple_adjoin_simple, normalClosure.restrictScalars_eq, LinearDisjoint.rank_right_mul_adjoin_rank_eq_of_isAlgebraic_right, restrictRestrictAlgEquivMapHom_surjective, AdjoinSimple.norm_gen_eq_one, range_val, instFiniteSubtypeMemBot, isCyclotomicExtension_lcm_sup, linearDisjoint_iff', splits_iff_mem, extendScalars.orderIso_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, AlgebraicIndependent.lift_reprField, isAlgebraic_adjoin, instIsLiouvilleSubtypeMemIntermediateField, SeparableClosure.hasEnoughRootsOfUnity_pow, IsTranscendenceBasis.isAlgebraic_field, PowerBasis.equivAdjoinSimple_aeval, extendScalars_adjoin, isPurelyInseparable_tower_bot, le_separableClosure_iff, charP', extendScalars_inf, botContinuousSMul, eq_separableClosure_iff, normal_iff_forall_fieldRange_le, IsGalois.normalAutEquivQuotient_apply, instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap, 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, LinearDisjoint.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic_right, InfiniteGalois.proj_adjoin_singleton_val, lift_inf, 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, Lifts.lt_iff, extendScalars_le_iff, instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, coe_sum, Splits.algebraicClosure, PowerBasis.equivAdjoinSimple_symm_gen, SeparableClosure.hasEnoughRootsOfUnity, coe_val, finrank_eq_finrank_subalgebra, finrank_eq_one_iff_eq_top, sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable', restrictRestrictAlgEquivMapHom_injective, Transcendental.algebraicClosure, 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, sepDegree_bot, normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure, trace_eq_sum_roots, finInsepDegree_bot', Algebra.norm_eq_norm_adjoin, isAlgebraic_adjoin_iff_isAlgebraic, 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, finrank_bot_mul_relfinrank, LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_right, finiteDimensional_adjoin, isTranscendenceBasis_adjoin_iff, lift_injective, coe_extendScalars, isSeparable_adjoin_simple_iff_isSeparable, AdjoinSimple.trace_gen_eq_zero, lift_sepDegree_bot', relrank_dvd_rank_top_of_le, 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, InfiniteGalois.isOpen_iff_finite, Field.Emb.Cardinal.deg_lt_aleph0, algHomAdjoinIntegralEquiv_symm_apply_gen, relfinrank_bot_left, le_extendScalars_iff, 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, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, spectralNorm.eq_of_normalClosure', finrank_fixedField_eq_card, separableClosure.isSepClosure, finrank_comap, InfiniteGalois.toAlgEquivAux_eq_liftNormal, normalClosure_def'', 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, Algebra.normalizedTrace_def, AdjoinSimple.isIntegral_gen, exists_lt_finrank_of_infinite_dimensional, Algebra.IsAlgebraic.isNormalClosure_normalClosure, isPurelyInseparable_bot, AlgebraicIndependent.aevalEquivField_apply_coe, LinearDisjoint.exists_field_of_isDomain, isSeparable_adjoin_pair_of_isSeparable, finiteDimensional_left, 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, 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, krullTopology_mem_nhds_one_iff, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin, krullTopology_mem_nhds_one_iff_of_normal, finrank_bot', isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, separableClosure.isSeparable, 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, extendScalars_restrictScalars, mem_extendScalars, perfectClosure.perfectField, FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMin, Field.Emb.Cardinal.instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, 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, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, lift_sup, normalClosure.normal, adjoin_adjoin_left, normalClosure_mono, separableClosure_le_iff, solvableByRad.isIntegral, 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, insepDegree_top, separableClosure_le_separableClosure_iff, transcendental_adjoin_iff, algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin_1, rank_comap, separableClosure.separableClosure_eq_bot, rank_bot_mul_relrank, finiteDimensional_map, 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, 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, isGalois_bot, intermediateFieldMap_symm_apply_coe, finrank_dvd_of_le_left, FG.exists_finset_maximalFor_isTranscendenceBasis_separableClosure, isGalois_iff_isGalois_bot, 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, finrank_adjoin_simple_eq_one_iff, isSeparable_tower_top, normalClosure.is_finiteDimensional, finiteDimensional_sup, Lifts.le_iff, trace_adjoinSimpleGen, normal_iff_normalClosure_eq, rank_adjoin_simple_eq_one_iff, isIntegral_iff, 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, perfectClosure.isPurelyInseparable, isSeparable_adjoin_iff_isSeparable, NumberField.hermiteTheorem.finite_of_discr_bdd_of_isReal, sepDegree_top, extendScalars_le_extendScalars_iff
toSubalgebra 📖	CompOp	49 math math: 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, 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, 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	26 math math: extendScalars_toSubfield, fieldRange_le, sSup_toSubfield, Subfield.extendScalars_toSubfield, iInf_toSubfield, coe_type_toSubfield, toSubfield_map, mem_toSubfield, AlgHom.fieldRange_toSubfield, coe_toSubfield, restrictScalars_toSubfield, Subfield.le_extendScalars_iff, Subfield.extendScalars_le_iff, iSup_toSubfield, toSubfield_inj, NumberField.linearDisjoint_of_isGalois_isCoprime_discr, bot_toSubfield, Subfield.toIntermediateField_toSubfield, top_toSubfield, adjoin_le_subfield, sInf_toSubfield, inf_toSubfield, Subfield.extendScalars.orderIso_symm_apply_coe, sup_toSubfield, adjoin_toSubfield, toSubfield_injective
val 📖	CompOp	11 math math: 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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
aeval_coe 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval IntermediateField SetLike.instMembership instSetLike toField algebra' Algebra.toSMul	—	Polynomial.aeval_algHom_apply AlgHom.algHomClass IsScalarTower.left isScalarTower
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom IntermediateField SetLike.instMembership instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing SubfieldClass.toSubringClass instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap toAlgebra	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
algebraMap_mem 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	—	Subalgebra.algebraMap_mem'
coe_add 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing SubfieldClass.toField instSubfieldClass	—	instSubfieldClass
coe_algebraMap_apply 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField RingHom.instFunLike algebraMap algebra' Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule	—	IsScalarTower.left
coe_copy 📖	mathematical	SetLike.coe IntermediateField instSetLike	copy	—	—
coe_equivMap_apply 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike map DFunLike.coe AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike equivMap AlgHom AlgHom.funLike	—	IsScalarTower.left
coe_extendScalars 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.coe SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars	—	—
coe_inclusion 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike inclusion	—	IsScalarTower.left
coe_inv 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike InvMemClass.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield SubfieldClass.toInvMemClass Field.toDivisionRing instSubfieldClass	—	SubfieldClass.toInvMemClass instSubfieldClass
coe_map 📖	mathematical	—	SetLike.coe IntermediateField instSetLike map Set.image DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike	—	—
coe_mul 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing SubfieldClass.toField instSubfieldClass	—	instSubfieldClass
coe_neg 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike NegMemClass.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing SubringClass.toNegMemClass SubfieldClass.toSubringClass instSubfieldClass	—	SubringClass.toNegMemClass SubfieldClass.toSubringClass instSubfieldClass
coe_one 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike OneMemClass.one AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass	—	AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
coe_pow 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike SubmonoidClass.nPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SubsemiringClass.toSubmonoidClass Semiring.toNonAssocSemiring SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing SubfieldClass.toSubringClass instSubfieldClass Monoid.toNatPow	—	SubmonoidClass.coe_pow SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
coe_prod 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike Finset.prod CommRing.toCommMonoid Field.toCommRing toField Finset.univ	—	SubmonoidClass.coe_finset_prod SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
coe_restrictScalars 📖	mathematical	—	SetLike.coe IntermediateField instSetLike restrictScalars	—	—
coe_smul 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike SetLike.smul' MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule Semifield.toCommSemiring instSMulMemClass	—	instSMulMemClass
coe_sum 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing toField Finset.univ	—	AddSubmonoidClass.coe_finset_sum SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
coe_toSubalgebra 📖	mathematical	—	SetLike.coe Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Subalgebra.instSetLike toSubalgebra IntermediateField instSetLike	—	—
coe_toSubfield 📖	mathematical	—	SetLike.coe Subfield Field.toDivisionRing Subfield.instSetLike toSubfield IntermediateField instSetLike	—	—
coe_type_toSubalgebra 📖	mathematical	—	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike toSubalgebra IntermediateField instSetLike	—	—
coe_type_toSubfield 📖	mathematical	—	Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike toSubfield IntermediateField instSetLike	—	—
coe_val 📖	mathematical	—	DFunLike.coe AlgHom IntermediateField SetLike.instMembership instSetLike Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike val	—	IsScalarTower.left
coe_zero 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SubsemiringClass.toAddSubmonoidClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass	—	AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
copy_eq 📖	mathematical	SetLike.coe IntermediateField instSetLike	copy	—	SetLike.coe_injective
div_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	div_mem SubfieldClass.toSubgroupClass instSubfieldClass
equivOfEq_apply 📖	mathematical	—	DFunLike.coe AlgEquiv IntermediateField SetLike.instMembership instSetLike Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike equivOfEq Subalgebra Subalgebra.instSetLike toSubalgebra	—	IsScalarTower.left
equivOfEq_rfl 📖	mathematical	—	equivOfEq IntermediateField AlgEquiv.refl SetLike.instMembership instSetLike Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule	—	AlgEquiv.ext IsScalarTower.left
equivOfEq_symm 📖	mathematical	—	AlgEquiv.symm IntermediateField SetLike.instMembership instSetLike Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule equivOfEq	—	IsScalarTower.left
equivOfEq_trans 📖	mathematical	—	AlgEquiv.trans IntermediateField SetLike.instMembership instSetLike Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule equivOfEq	—	IsScalarTower.left
ext 📖	—	IntermediateField SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike	—	ext
extendScalars_injective 📖	mathematical	—	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars	—	OrderIso.injective
extendScalars_le_extendScalars_iff 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars	—	—
extendScalars_le_iff 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars restrictScalars algebra' Algebra.toSMul CommSemiring.toSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule isScalarTower_mid'	—	—
extendScalars_restrictScalars 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	restrictScalars SetLike.instMembership instSetLike toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule instAlgebraSubtypeMem isScalarTower_mid' extendScalars	—	IsScalarTower.left isScalarTower_mid'
extendScalars_toSubfield 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	toSubfield SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars	—	SetLike.coe_injective
fieldRange_comp_val 📖	mathematical	—	AlgHom.fieldRange IntermediateField SetLike.instMembership instSetLike toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgHom.comp val map	—	toSubalgebra_injective IsScalarTower.left toSubalgebra_map AlgHom.fieldRange_toSubalgebra AlgHom.range_comp range_val
fieldRange_le 📖	mathematical	—	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder Subfield.instPartialOrder RingHom.fieldRange algebraMap Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toSubfield	—	Subalgebra.range_subset Set.mem_range RingHom.mem_fieldRange
fieldRange_val 📖	mathematical	—	AlgHom.fieldRange IntermediateField SetLike.instMembership instSetLike toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule val	—	SetLike.ext' IsScalarTower.left Subtype.range_val
gc_map_comap 📖	mathematical	—	GaloisConnection IntermediateField PartialOrder.toPreorder instPartialOrder map comap	—	map_le_iff_le_comap
inclusion_inclusion 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe AlgHom SetLike.instMembership instSetLike Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike inclusion le_trans	—	Subalgebra.inclusion_inclusion
inclusion_injective 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike inclusion	—	Subalgebra.inclusion_injective
inclusion_self 📖	mathematical	—	inclusion le_refl IntermediateField PartialOrder.toPreorder instPartialOrder AlgHom.id SetLike.instMembership instSetLike Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule	—	Subalgebra.inclusion_self
instFaithfulSMulSubtypeMem 📖	mathematical	—	FaithfulSMul IntermediateField SetLike.instMembership instSetLike instSMulSubtypeMem	—	Subfield.instFaithfulSMulSubtypeMem
instIsScalarTowerSubtypeMem 📖	mathematical	—	IsScalarTower IntermediateField SetLike.instMembership instSetLike instSMulSubtypeMem	—	Subfield.instIsScalarTowerSubtypeMem
instIsScalarTowerSubtypeMem_1 📖	mathematical	—	IsScalarTower IntermediateField SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.toSMul Semifield.toCommSemiring algebra' CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule instSMulSubtypeMem_1 isScalarTower_mid	—	isScalarTower IsScalarTower.left isScalarTower_mid
instSMulMemClass 📖	mathematical	—	SMulMemClass IntermediateField Algebra.toSMul Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring instSetLike	—	smul_mem
instSubfieldClass 📖	mathematical	—	SubfieldClass IntermediateField Field.toDivisionRing instSetLike	—	Subsemigroup.mul_mem' Submonoid.one_mem' Subsemiring.add_mem' Subsemiring.zero_mem' neg_mem inv_mem'
intCast_mem 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	intCast_mem SubfieldClass.toSubringClass instSubfieldClass
intermediateFieldMap_apply_coe 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike map AlgEquiv.toAlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring DFunLike.coe AlgEquiv toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike intermediateFieldMap	—	IsScalarTower.left
intermediateFieldMap_symm_apply_coe 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike DFunLike.coe AlgEquiv map AlgEquiv.toAlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike AlgEquiv.symm intermediateFieldMap	—	IsScalarTower.left
inv_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	InvMemClass.inv_mem SubfieldClass.toInvMemClass instSubfieldClass
inv_mem' 📖	mathematical	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submonoid.toSubsemigroup Subsemiring.toSubmonoid Subalgebra.toSubsemiring Semifield.toCommSemiring toSubalgebra	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	—
isScalarTower 📖	mathematical	—	IsScalarTower IntermediateField SetLike.instMembership instSetLike Algebra.toSMul Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul module'	—	Subalgebra.instIsScalarTowerSubtypeMem
isScalarTower_bot 📖	mathematical	—	IsScalarTower IntermediateField SetLike.instMembership instSetLike instSMulSubtypeMem Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id	—	IsScalarTower.subalgebra
isScalarTower_mid 📖	mathematical	—	IsScalarTower IntermediateField SetLike.instMembership instSetLike Algebra.toSMul Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule instSMulSubtypeMem	—	IsScalarTower.subalgebra'
isScalarTower_mid' 📖	mathematical	—	IsScalarTower IntermediateField SetLike.instMembership instSetLike Algebra.toSMul Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule instSMulSubtypeMem	—	IsScalarTower.left isScalarTower_mid IsScalarTower.right
le_extendScalars_iff 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars restrictScalars algebra' Algebra.toSMul CommSemiring.toSemiring IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule isScalarTower_mid'	—	—
liftAlgEquiv_apply 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike lift DFunLike.coe AlgEquiv toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule isScalarTower AlgEquiv.instFunLike liftAlgEquiv	—	IsScalarTower.left isScalarTower
lift_inj 📖	mathematical	—	lift	—	IsScalarTower.left lift_injective
lift_injective 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule lift	—	map_injective IsScalarTower.left
lift_le 📖	mathematical	—	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder lift	—	IsScalarTower.left
lift_restrict 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	lift restrict	—	ext lift_le IsScalarTower.left mem_restrict mem_lift
list_prod_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	list_prod_mem SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
list_sum_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	list_sum_mem SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
map_id 📖	mathematical	—	map AlgHom.id Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	SetLike.coe_injective Set.image_id
map_injective 📖	mathematical	—	IntermediateField map	—	Subalgebra.map_injective RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing toSubalgebra_map toSubalgebra_injective
map_le_iff_le_comap 📖	mathematical	—	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder map comap	—	Set.image_subset_iff
map_map 📖	mathematical	—	map AlgHom.comp Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	SetLike.coe_injective Set.image_image
map_mono 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	map	—	SetLike.coe_mono instIsConcreteLE Set.image_mono
mem_carrier 📖	mathematical	—	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submonoid.toSubsemigroup Subsemiring.toSubmonoid Subalgebra.toSubsemiring Semifield.toCommSemiring toSubalgebra IntermediateField SetLike.instMembership instSetLike	—	—
mem_extendScalars 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike toField instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring extendScalars	—	—
mem_lift 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike lift toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule	—	IsScalarTower.left Function.Injective.mem_set_image Subtype.val_injective
mem_mk 📖	mathematical	Subsemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SetLike.instMembership Subsemiring.instSetLike DFunLike.coe RingHom CommSemiring.toSemiring Semifield.toCommSemiring RingHom.instFunLike algebraMap Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.toSubsemigroup Subsemiring.toSubmonoid Subalgebra.toSubsemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	IntermediateField instSetLike	—	—
mem_restrict 📖	mathematical	IntermediateField Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.instMembership instSetLike toField algebra' Semifield.toCommSemiring Field.toSemifield Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule restrict	—	Set.ext_iff Set.range_inclusion
mem_restrictScalars 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike restrictScalars	—	—
mem_toSubalgebra 📖	mathematical	—	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike toSubalgebra IntermediateField instSetLike	—	—
mem_toSubfield 📖	mathematical	—	Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike toSubfield IntermediateField instSetLike	—	—
mul_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
multiset_prod_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Multiset.prod CommRing.toCommMonoid Field.toCommRing	—	multiset_prod_mem SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
multiset_sum_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	multiset_sum_mem SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
natCast_mem 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	SubsemiringClass.addSubmonoidWithOneClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
neg_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup DivisionRing.toRing Field.toDivisionRing	—	SubringClass.toNegMemClass Subalgebra.instSubringClass
one_mem 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	OneMemClass.one_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
pow_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	DivInvMonoid.toZPow DivisionRing.toDivInvMonoid Field.toDivisionRing	—	zpow_mem SubfieldClass.toSubgroupClass instSubfieldClass
prod_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Finset.prod CommRing.toCommMonoid Field.toCommRing	—	prod_mem SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
range_val 📖	mathematical	—	AlgHom.range IntermediateField SetLike.instMembership instSetLike Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule val toSubalgebra	—	Subalgebra.range_val
restrictScalars_inj 📖	mathematical	—	restrictScalars	—	restrictScalars_injective
restrictScalars_injective 📖	mathematical	—	IntermediateField restrictScalars	—	ext mem_restrictScalars
restrictScalars_toSubalgebra 📖	mathematical	—	toSubalgebra restrictScalars Subalgebra.restrictScalars Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	SetLike.coe_injective
restrictScalars_toSubfield 📖	mathematical	—	toSubfield restrictScalars	—	SetLike.coe_injective
set_range_subset 📖	mathematical	—	Set Set.instHasSubset Set.range DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap SetLike.coe IntermediateField instSetLike	—	Subalgebra.range_subset
smulCommClass_left 📖	mathematical	—	SMulCommClass IntermediateField SetLike.instMembership instSetLike instSMulSubtypeMem	—	Subfield.smulCommClass_left
smulCommClass_right 📖	mathematical	—	SMulCommClass IntermediateField SetLike.instMembership instSetLike instSMulSubtypeMem	—	Subfield.smulCommClass_right
smul_def 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike instSMulSubtypeMem	—	—
smul_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Algebra.toSMul Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Subalgebra.smul_mem
sub_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	sub_mem SubringClass.addSubgroupClass SubfieldClass.toSubringClass instSubfieldClass
sum_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	sum_mem SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
toSubalgebra_inj 📖	mathematical	—	toSubalgebra	—	toSubalgebra_injective
toSubalgebra_injective 📖	mathematical	—	IntermediateField Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toSubalgebra	—	ext
toSubalgebra_le_toSubalgebra 📖	mathematical	—	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder toSubalgebra IntermediateField instPartialOrder	—	—
toSubalgebra_lt_toSubalgebra 📖	mathematical	—	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Preorder.toLT PartialOrder.toPreorder Subalgebra.instPartialOrder toSubalgebra IntermediateField instPartialOrder	—	—
toSubalgebra_map 📖	mathematical	—	toSubalgebra map Subalgebra.map Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	—
toSubalgebra_strictMono 📖	mathematical	—	StrictMono IntermediateField Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring PartialOrder.toPreorder instPartialOrder Subalgebra.instPartialOrder toSubalgebra	—	—
toSubfield_inj 📖	mathematical	—	toSubfield	—	toSubfield_injective
toSubfield_injective 📖	mathematical	—	IntermediateField Subfield Field.toDivisionRing toSubfield	—	ext
toSubfield_map 📖	mathematical	—	toSubfield map Subfield.map Field.toDivisionRing RingHomClass.toRingHom AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgHom.funLike Semiring.toNonAssocSemiring DivisionRing.toDivisionSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	—
val_mk 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	DFunLike.coe AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring toField algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Module.toDistribMulAction Algebra.toModule AlgHom.funLike val	—	IsScalarTower.left
zero_mem 📖	mathematical	—	IntermediateField SetLike.instMembership instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	—	ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass instSubfieldClass
zsmul_mem 📖	mathematical	IntermediateField SetLike.instMembership instSetLike	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	zsmul_mem SubringClass.addSubgroupClass SubfieldClass.toSubringClass instSubfieldClass

IntermediateField.AlgHom

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—

IntermediateField.extendScalars

Definitions

Name	Category	Theorems
orderIso 📖	CompOp	2 math math: orderIso_apply, orderIso_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderIso_apply 📖	mathematical	—	DFunLike.coe RelIso IntermediateField Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField IntermediateField.instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring RelIso.instFunLike orderIso IntermediateField.extendScalars	—	—
orderIso_symm_apply_coe 📖	mathematical	—	IntermediateField Preorder.toLE PartialOrder.toPreorder IntermediateField.instPartialOrder DFunLike.coe RelIso SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField IntermediateField.instAlgebraSubtypeMem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Algebra.id Semifield.toCommSemiring RelIso.instFunLike RelIso.symm orderIso IntermediateField.restrictScalars IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring IntermediateField.isScalarTower_mid'	—	—

Subalgebra

Definitions

Name	Category	Theorems
toIntermediateField 📖	CompOp	2 math math: toIntermediateField_toSubalgebra, toSubalgebra_toIntermediateField
toIntermediateField' 📖	CompOp	2 math math: toSubalgebra_toIntermediateField', toIntermediateField'_toSubalgebra

Subfield

Definitions

Name	Category	Theorems
extendScalars 📖	CompOp	14 math math: extendScalars_toSubfield, relfinrank_eq_finrank_of_le, extendScalars_le_extendScalars_iff, extendScalars_inf, extendScalars_top, le_extendScalars_iff, extendScalars_le_iff, extendScalars.orderIso_apply, relrank_eq_rank_of_le, extendScalars_sup, extendScalars_self, mem_extendScalars, coe_extendScalars, extendScalars_injective
toIntermediateField 📖	CompOp	2 math math: coe_toIntermediateField, toIntermediateField_toSubfield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_extendScalars 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	SetLike.coe IntermediateField SetLike.instMembership instSetLike toField toAlgebra IntermediateField.instSetLike extendScalars	—	—
coe_toIntermediateField 📖	mathematical	Subfield Field.toDivisionRing SetLike.instMembership instSetLike DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	SetLike.coe IntermediateField IntermediateField.instSetLike toIntermediateField	—	—
extendScalars_injective 📖	mathematical	—	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder IntermediateField SetLike.instMembership instSetLike toField toAlgebra extendScalars	—	OrderIso.injective
extendScalars_le_extendScalars_iff 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	IntermediateField SetLike.instMembership instSetLike toField toAlgebra IntermediateField.instPartialOrder extendScalars	—	—
extendScalars_le_iff 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	IntermediateField SetLike.instMembership instSetLike toField toAlgebra IntermediateField.instPartialOrder extendScalars IntermediateField.toSubfield	—	—
extendScalars_toSubfield 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	IntermediateField.toSubfield SetLike.instMembership instSetLike toField toAlgebra extendScalars	—	SetLike.coe_injective
le_extendScalars_iff 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	IntermediateField SetLike.instMembership instSetLike toField toAlgebra IntermediateField.instPartialOrder extendScalars IntermediateField.toSubfield	—	—
mem_extendScalars 📖	mathematical	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder instPartialOrder	IntermediateField SetLike.instMembership instSetLike toField toAlgebra IntermediateField.instSetLike extendScalars	—	—
toIntermediateField_toSubfield 📖	mathematical	Subfield Field.toDivisionRing SetLike.instMembership instSetLike DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap	IntermediateField.toSubfield toIntermediateField	—	—

Subfield.extendScalars

Definitions

Name	Category	Theorems
orderIso 📖	CompOp	2 math math: orderIso_apply, orderIso_symm_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
orderIso_apply 📖	mathematical	—	DFunLike.coe RelIso Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder Subfield.instPartialOrder IntermediateField SetLike.instMembership Subfield.instSetLike Subfield.toField Subfield.toAlgebra IntermediateField.instPartialOrder RelIso.instFunLike orderIso Subfield.extendScalars	—	—
orderIso_symm_apply_coe 📖	mathematical	—	Subfield Field.toDivisionRing Preorder.toLE PartialOrder.toPreorder Subfield.instPartialOrder DFunLike.coe RelIso IntermediateField SetLike.instMembership Subfield.instSetLike Subfield.toField Subfield.toAlgebra IntermediateField.instPartialOrder RelIso.instFunLike RelIso.symm orderIso IntermediateField.toSubfield	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIntermediateField'_toSubalgebra 📖	mathematical	—	Subalgebra.toIntermediateField' IntermediateField.toSubalgebra Field.toIsField IntermediateField SetLike.instMembership IntermediateField.instSetLike SubfieldClass.toField IntermediateField.instSubfieldClass	—	IntermediateField.ext Field.toIsField IntermediateField.instSubfieldClass
toIntermediateField_toSubalgebra 📖	mathematical	—	Subalgebra.toIntermediateField IntermediateField.toSubalgebra IntermediateField.inv_mem	—	IntermediateField.ext IntermediateField.inv_mem
toSubalgebra_toIntermediateField 📖	mathematical	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	IntermediateField.toSubalgebra Subalgebra.toIntermediateField	—	Subalgebra.ext
toSubalgebra_toIntermediateField' 📖	mathematical	IsField Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Subalgebra.toSemiring	IntermediateField.toSubalgebra Subalgebra.toIntermediateField'	—	Subalgebra.ext

---

← Back to Index