Commit 2023-06-08 11:30 832c78a6

View on Github →

feat: port FieldTheory.Adjoin (#4723)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Adjoin.lean

added theorem IntermediateField.AdjoinSimple.algebraMap_gen

added def IntermediateField.AdjoinSimple.gen

added theorem IntermediateField.AdjoinSimple.isIntegral_gen

added theorem IntermediateField.AlgEquiv.fieldRange_eq_top

added theorem IntermediateField.AlgHom.fieldRange_eq_map

added theorem IntermediateField.AlgHom.fieldRange_eq_top

added theorem IntermediateField.AlgHom.map_fieldRange

added def IntermediateField.FG

added theorem IntermediateField.Lifts.eq_of_le

added theorem IntermediateField.Lifts.exists_lift_of_splits

added theorem IntermediateField.Lifts.exists_max_three

added theorem IntermediateField.Lifts.exists_max_two

added theorem IntermediateField.Lifts.exists_upper_bound

added theorem IntermediateField.Lifts.le_lifts_of_splits

added theorem IntermediateField.Lifts.mem_lifts_of_splits

added def IntermediateField.Lifts.upperBoundIntermediateField

added def IntermediateField.Lifts

added theorem IntermediateField.adjoin.algebraMap_mem

added theorem IntermediateField.adjoin.finiteDimensional

added theorem IntermediateField.adjoin.finrank

added theorem IntermediateField.adjoin.mono

added theorem IntermediateField.adjoin.range_algebraMap_subset

added def IntermediateField.adjoin

added theorem IntermediateField.adjoinRootEquivAdjoin_apply_root

added theorem IntermediateField.adjoin_adjoin_comm

added theorem IntermediateField.adjoin_adjoin_left

added theorem IntermediateField.adjoin_algebraic_toSubalgebra

added theorem IntermediateField.adjoin_contains_field_as_subfield

added theorem IntermediateField.adjoin_empty

added theorem IntermediateField.adjoin_eq_algebra_adjoin

added theorem IntermediateField.adjoin_eq_bot_iff

added theorem IntermediateField.adjoin_eq_range_algebraMap_adjoin

added theorem IntermediateField.adjoin_finite_isCompactElement

added theorem IntermediateField.adjoin_finset_isCompactElement

added theorem IntermediateField.adjoin_induction

added theorem IntermediateField.adjoin_insert_adjoin

added theorem IntermediateField.adjoin_int

added theorem IntermediateField.adjoin_le_iff

added theorem IntermediateField.adjoin_le_subfield

added theorem IntermediateField.adjoin_map

added theorem IntermediateField.adjoin_nat

added theorem IntermediateField.adjoin_one

added theorem IntermediateField.adjoin_rootSet_isSplittingField

added theorem IntermediateField.adjoin_simple_adjoin_simple

added theorem IntermediateField.adjoin_simple_comm

added theorem IntermediateField.adjoin_simple_eq_bot_iff

added theorem IntermediateField.adjoin_simple_isCompactElement

added theorem IntermediateField.adjoin_simple_le_iff

added theorem IntermediateField.adjoin_simple_toSubalgebra_of_integral

added theorem IntermediateField.adjoin_subset_adjoin_iff

added theorem IntermediateField.adjoin_univ

added theorem IntermediateField.adjoin_zero

added theorem IntermediateField.aeval_gen_minpoly

added theorem IntermediateField.algHom_mk_adjoin_splits'

added theorem IntermediateField.algHom_mk_adjoin_splits

added theorem IntermediateField.algebra_adjoin_le_adjoin

added theorem IntermediateField.botEquiv_def

added theorem IntermediateField.botEquiv_symm

added theorem IntermediateField.bot_eq_top_of_finrank_adjoin_eq_one

added theorem IntermediateField.bot_eq_top_of_finrank_adjoin_le_one

added theorem IntermediateField.bot_eq_top_of_rank_adjoin_eq_one

added theorem IntermediateField.bot_toSubalgebra

added theorem IntermediateField.card_algHom_adjoin_integral

added theorem IntermediateField.coe_algebraMap_over_bot

added theorem IntermediateField.coe_bot

added theorem IntermediateField.coe_iInf

added theorem IntermediateField.coe_inf

added theorem IntermediateField.coe_sInf

added theorem IntermediateField.coe_top

added theorem IntermediateField.eq_adjoin_of_eq_algebra_adjoin

added def IntermediateField.equivOfEq

added theorem IntermediateField.equivOfEq_rfl

added theorem IntermediateField.equivOfEq_symm

added theorem IntermediateField.equivOfEq_trans

added theorem IntermediateField.exists_finset_of_mem_iSup

added theorem IntermediateField.exists_finset_of_mem_supr''

added theorem IntermediateField.exists_finset_of_mem_supr'

added theorem IntermediateField.fG_of_fG_toSubalgebra

added theorem IntermediateField.fg_adjoin_finset

added theorem IntermediateField.fg_bot

added theorem IntermediateField.fg_def

added theorem IntermediateField.fg_of_noetherian

added theorem IntermediateField.finiteDimensional_iSup_of_finset'

added theorem IntermediateField.finrank_adjoin_eq_one_iff

added theorem IntermediateField.finrank_adjoin_simple_eq_one_iff

added theorem IntermediateField.finrank_bot

added theorem IntermediateField.finrank_eq_one_iff

added theorem IntermediateField.gc

added def IntermediateField.gi

added theorem IntermediateField.iInf_toSubalgebra

added theorem IntermediateField.iInf_toSubfield

added theorem IntermediateField.induction_on_adjoin

added theorem IntermediateField.induction_on_adjoin_fg

added theorem IntermediateField.induction_on_adjoin_finset

added theorem IntermediateField.inf_toSubalgebra

added theorem IntermediateField.inf_toSubfield

added theorem IntermediateField.insert_le_iff

added theorem IntermediateField.isAlgebraic_iSup

added theorem IntermediateField.isSplittingField_iSup

added theorem IntermediateField.isSplittingField_iff

added theorem IntermediateField.le_sup_toSubalgebra

added theorem IntermediateField.mem_adjoin_simple_self

added theorem IntermediateField.mem_bot

added theorem IntermediateField.mem_inf

added theorem IntermediateField.mem_top

added theorem IntermediateField.minpoly.degree_le

added theorem IntermediateField.minpoly.natDegree_le

added theorem IntermediateField.minpoly_gen

added theorem IntermediateField.rank_adjoin_eq_one_iff

added theorem IntermediateField.rank_adjoin_simple_eq_one_iff

added theorem IntermediateField.rank_bot

added theorem IntermediateField.rank_eq_one_iff

added theorem IntermediateField.restrictScalars_bot_eq_self

added theorem IntermediateField.restrictScalars_top

added theorem IntermediateField.sInf_toSubalgebra

added theorem IntermediateField.sInf_toSubfield

added theorem IntermediateField.subset_adjoin

added theorem IntermediateField.subset_adjoin_of_subset_left

added theorem IntermediateField.subset_adjoin_of_subset_right

added theorem IntermediateField.subsingleton_of_finrank_adjoin_eq_one

added theorem IntermediateField.subsingleton_of_finrank_adjoin_le_one

added theorem IntermediateField.subsingleton_of_rank_adjoin_eq_one

added theorem IntermediateField.sup_toSubalgebra

added def IntermediateField.topEquiv

added theorem IntermediateField.top_toSubalgebra

added theorem IntermediateField.top_toSubfield

added theorem PowerBasis.equivAdjoinSimple_aeval

added theorem PowerBasis.equivAdjoinSimple_gen

added theorem PowerBasis.equivAdjoinSimple_symm_aeval

added theorem PowerBasis.equivAdjoinSimple_symm_gen