Commit 2023-11-10 09:13 0ffba7e4

View on Github →

feat(FieldTheory/PrimitiveElement): Steinitz Theorem (#7788) Added Field.exists_primitive_element_iff_finite_intermediateField: a finite extension E / F has a primitive element if and only if the intermediate fields between E / F are finitely many. Also known as Steinitz Theorem https://en.wikipedia.org/wiki/Primitive_element_theorem#The_theorems.

Estimated changes

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem IntermediateField.adjoin_eq_top_of_adjoin_eq_top

added theorem IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element

added theorem IntermediateField.adjoin_self

added theorem IntermediateField.finiteDimensional_adjoin_of_finite_of_isAlgebraic

added theorem IntermediateField.lift_adjoin

added theorem IntermediateField.lift_adjoin_simple

added theorem IntermediateField.lift_bot

added theorem IntermediateField.lift_top

added theorem IntermediateField.mem_adjoin_iff

added theorem IntermediateField.mem_adjoin_simple_iff

added theorem IntermediateField.restrictScalars_adjoin

Modified Mathlib/FieldTheory/PrimitiveElement.lean

added theorem Field.exists_primitive_element_iff_finite_intermediateField

added theorem Field.exists_primitive_element_of_finite_intermediateField

added theorem Field.finiteDimensional_of_exists_primitive_element

added theorem Field.finiteDimensional_of_finite_intermediateField

added theorem Field.finite_intermediateField_of_exists_primitive_element

added theorem Field.isAlgebraic_of_adjoin_eq_adjoin

added theorem Field.isAlgebraic_of_finite_intermediateField

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified docs/overview.yaml

Modified docs/undergrad.yaml