Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-12 12:21 1362701b

View on Github →

refactor(field_theory): Adjoin intermediate field (#4468) Refactor adjoin to be an intermediate field rather than a subalgebra.

Estimated changes

Modified src/field_theory/adjoin.lean

deleted theorem field.adjoin.algebra_map_mem

deleted theorem field.adjoin.mono

deleted theorem field.adjoin.range_algebra_map_subset

deleted def field.adjoin

deleted theorem field.adjoin_adjoin_comm

deleted theorem field.adjoin_adjoin_left

deleted theorem field.adjoin_contains_field_as_subfield

deleted theorem field.adjoin_dim_eq_one_iff

deleted theorem field.adjoin_dim_eq_one_of_sub_bot

deleted theorem field.adjoin_eq_bot

deleted theorem field.adjoin_eq_bot_iff

deleted theorem field.adjoin_eq_range_algebra_map_adjoin

deleted theorem field.adjoin_findim_eq_one_iff

deleted theorem field.adjoin_one

deleted theorem field.adjoin_simple.algebra_map_gen

deleted def field.adjoin_simple.gen

deleted theorem field.adjoin_simple_adjoin_simple

deleted theorem field.adjoin_simple_comm

deleted theorem field.adjoin_simple_dim_eq_one_iff

deleted theorem field.adjoin_simple_dim_eq_one_of_mem_bot

deleted theorem field.adjoin_simple_eq_bot

deleted theorem field.adjoin_simple_eq_bot_iff

deleted theorem field.adjoin_simple_findim_eq_one_iff

deleted theorem field.adjoin_subset_adjoin_iff

deleted theorem field.adjoin_subset_iff

deleted theorem field.adjoin_subset_subfield

deleted theorem field.adjoin_zero

deleted theorem field.bot_eq_top_of_dim_adjoin_eq_one

deleted theorem field.bot_eq_top_of_findim_adjoin_eq_one

deleted theorem field.bot_eq_top_of_findim_adjoin_le_one

deleted theorem field.mem_adjoin_simple_self

deleted theorem field.mem_bot_of_adjoin_simple_dim_eq_one

deleted theorem field.mem_bot_of_adjoin_simple_sub_bot

deleted theorem field.sub_bot_of_adjoin_dim_eq_one

deleted theorem field.sub_bot_of_adjoin_sub_bot

deleted theorem field.subfield_subset_adjoin_self

deleted theorem field.subset_adjoin

deleted theorem field.subset_adjoin_of_subset_left

deleted theorem field.subset_adjoin_of_subset_right

added theorem intermediate_field.adjoin.algebra_map_mem

added theorem intermediate_field.adjoin.mono

added theorem intermediate_field.adjoin.range_algebra_map_subset

added def intermediate_field.adjoin

added theorem intermediate_field.adjoin_adjoin_comm

added theorem intermediate_field.adjoin_adjoin_left

added theorem intermediate_field.adjoin_contains_field_as_subfield

added theorem intermediate_field.adjoin_eq_bot_iff

added theorem intermediate_field.adjoin_eq_range_algebra_map_adjoin

added theorem intermediate_field.adjoin_induction

added theorem intermediate_field.adjoin_int

added theorem intermediate_field.adjoin_le_algebra_adjoin

added theorem intermediate_field.adjoin_le_iff

added theorem intermediate_field.adjoin_le_subfield

added theorem intermediate_field.adjoin_map

added theorem intermediate_field.adjoin_nat

added theorem intermediate_field.adjoin_one

added theorem intermediate_field.adjoin_simple.algebra_map_gen

added def intermediate_field.adjoin_simple.gen

added theorem intermediate_field.adjoin_simple_adjoin_simple

added theorem intermediate_field.adjoin_simple_comm

added theorem intermediate_field.adjoin_simple_eq_bot_iff

added theorem intermediate_field.adjoin_subset_adjoin_iff

added theorem intermediate_field.adjoin_zero

added theorem intermediate_field.algebra_adjoin_le_adjoin

added theorem intermediate_field.bot_eq_top_of_dim_adjoin_eq_one

added theorem intermediate_field.bot_eq_top_of_findim_adjoin_eq_one

added theorem intermediate_field.bot_eq_top_of_findim_adjoin_le_one

added theorem intermediate_field.bot_to_subalgebra

added theorem intermediate_field.coe_bot_eq_self

added theorem intermediate_field.coe_top_eq_top

added theorem intermediate_field.dim_adjoin_eq_one_iff

added theorem intermediate_field.dim_adjoin_simple_eq_one_iff

added theorem intermediate_field.dim_intermediate_field_eq_dim_subalgebra

added theorem intermediate_field.findim_adjoin_eq_one_iff

added theorem intermediate_field.findim_adjoin_simple_eq_one_iff

added theorem intermediate_field.findim_intermediate_field_eq_findim_subalgebra

added theorem intermediate_field.gc

added def intermediate_field.gi

added theorem intermediate_field.induction_on_adjoin

added theorem intermediate_field.mem_adjoin_simple_self

added theorem intermediate_field.mem_bot

added theorem intermediate_field.mem_top

added theorem intermediate_field.subset_adjoin

added theorem intermediate_field.subset_adjoin_of_subset_left

added theorem intermediate_field.subset_adjoin_of_subset_right

added theorem intermediate_field.subsingleton_of_dim_adjoin_eq_one

added theorem intermediate_field.subsingleton_of_findim_adjoin_eq_one

added theorem intermediate_field.subsingleton_of_findim_adjoin_le_one

added theorem intermediate_field.to_subalgebra_eq_iff

added theorem intermediate_field.top_to_subalgebra

Modified src/field_theory/intermediate_field.lean

added def intermediate_field.lift1

added def intermediate_field.lift2

added theorem intermediate_field.mem_lift2

modified theorem intermediate_field.pow_mem

Modified src/field_theory/primitive_element.lean

deleted theorem field.exists_primitive_element_aux

deleted theorem field.exists_primitive_element_inf

Modified src/field_theory/subfield.lean

Modified src/order/bounded_lattice.lean

added theorem eq_bot_of_bot_eq_top

added theorem eq_top_of_bot_eq_top

added theorem subsingleton_of_bot_eq_top