Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-26 19:15 253b120d

View on Github →

feat(field_theory): prove primitive element theorem (#4153) Proof of the primitive element theorem. The main proof is in field_theory/primitive_element.lean. Some lemmas we used have been added to other files. We have also changed the notation for adjoining an element to a field to be easier to use.

Estimated changes

Modified src/data/polynomial/field_division.lean

added theorem polynomial.eval_gcd_eq_zero

added theorem polynomial.eval₂_gcd_eq_zero

added theorem polynomial.is_root_gcd_iff_is_root_left_right

added theorem polynomial.mem_roots_map

added theorem polynomial.root_gcd_iff_root_left_right

added theorem polynomial.root_left_of_root_gcd

added theorem polynomial.root_right_of_root_gcd

Modified src/deprecated/subfield.lean

added theorem is_subfield.pow_mem

Modified src/field_theory/adjoin.lean

added theorem field.adjoin_adjoin_comm

added theorem field.adjoin_dim_eq_one_iff

added theorem field.adjoin_dim_eq_one_of_sub_bot

added theorem field.adjoin_eq_bot

added theorem field.adjoin_eq_bot_iff

added theorem field.adjoin_eq_range_algebra_map_adjoin

added theorem field.adjoin_findim_eq_one_iff

added theorem field.adjoin_one

modified theorem field.adjoin_simple.algebra_map_gen

modified theorem field.adjoin_simple_adjoin_simple

added theorem field.adjoin_simple_comm

added theorem field.adjoin_simple_dim_eq_one_iff

added theorem field.adjoin_simple_dim_eq_one_of_mem_bot

added theorem field.adjoin_simple_eq_bot

added theorem field.adjoin_simple_eq_bot_iff

added theorem field.adjoin_simple_findim_eq_one_iff

deleted theorem field.adjoin_singleton

added theorem field.adjoin_zero

added theorem field.bot_eq_top_of_dim_adjoin_eq_one

added theorem field.bot_eq_top_of_findim_adjoin_eq_one

added theorem field.bot_eq_top_of_findim_adjoin_le_one

added theorem field.mem_bot_of_adjoin_simple_dim_eq_one

added theorem field.mem_bot_of_adjoin_simple_sub_bot

added theorem field.sub_bot_of_adjoin_dim_eq_one

added theorem field.sub_bot_of_adjoin_sub_bot

Modified src/field_theory/minimal_polynomial.lean

added theorem minimal_polynomial.dvd_map_of_is_scalar_tower

Created src/field_theory/primitive_element.lean

added theorem field.exists_primitive_element

added theorem field.exists_primitive_element_aux

added theorem field.exists_primitive_element_inf

added theorem field.exists_primitive_element_of_fintype_bot

added theorem field.exists_primitive_element_of_fintype_top

added theorem field.primitive_element_inf_aux

added theorem field.primitive_element_inf_aux_exists_c

Modified src/field_theory/separable.lean

added theorem is_separable_tower_bot_of_is_separable

added theorem is_separable_tower_top_of_is_separable

added theorem polynomial.eq_X_sub_C_of_separable_of_root_eq

added theorem polynomial.separable_gcd_left

added theorem polynomial.separable_gcd_right

Modified src/field_theory/splitting_field.lean

added theorem polynomial.eq_X_sub_C_of_splits_of_single_root

added theorem polynomial.splits_of_splits_gcd_left

added theorem polynomial.splits_of_splits_gcd_right

Modified src/linear_algebra/finite_dimensional.lean

modified theorem findim_top

added theorem finite_dimensional_of_dim_eq_one

added theorem subalgebra.bot_eq_top_of_dim_eq_one

added theorem subalgebra.bot_eq_top_of_findim_eq_one

added theorem subalgebra.dim_bot

added theorem subalgebra.dim_eq_one_iff

added theorem subalgebra.dim_eq_one_of_eq_bot

added theorem subalgebra.dim_top

added theorem subalgebra.eq_bot_of_dim_one

added theorem subalgebra.eq_bot_of_findim_one

added theorem subalgebra.findim_bot

added theorem subalgebra.findim_eq_one_iff

added theorem subalgebra.findim_eq_one_of_eq_bot

added theorem subalgebra.finite_dimensional_bot

added theorem subalgebra_top_dim_eq_submodule_top_dim

added theorem subalgebra_top_findim_eq_submodule_top_findim

Modified src/ring_theory/algebra.lean

added theorem algebra.coe_bot

Modified src/ring_theory/algebra_tower.lean

added theorem is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero

added theorem is_scalar_tower.aeval_eq_zero_of_aeval_algebra_map_eq_zero_field

added theorem is_scalar_tower.algebra_map_aeval

Modified src/ring_theory/integral_closure.lean

added theorem is_integral_tower_bot_of_is_integral_field