Commit 2023-12-10 15:17 38c82baa

View on Github →

feat: Add some equivalent characterisations of primitive elements in finite extensions of fields (#8609) See the Zulip thread

Estimated changes

Modified Mathlib/Data/Polynomial/Splits.lean

added theorem Polynomial.splits_of_algHom

added theorem Polynomial.splits_of_isScalarTower

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

added theorem Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed_apply_apply

modified theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly

added def IntermediateField.algHomEquivAlgHomOfIsAlgClosed

added theorem IntermediateField.algHomEquivAlgHomOfIsAlgClosed_apply_apply

Modified Mathlib/FieldTheory/PrimitiveElement.lean

modified theorem AlgHom.card

added theorem AlgHom.card_of_splits

added theorem Field.primitive_element_iff_algHom_eq_of_eval'

added theorem Field.primitive_element_iff_algHom_eq_of_eval

added theorem Field.primitive_element_iff_minpoly_degree_eq

added theorem Field.primitive_element_iff_minpoly_natDegree_eq