Commit 2024-01-11 20:30 3e1faebb

View on Github →

chore: split IntermediateField.Lifts out of FieldTheory/Adjoin (#9647)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Adjoin.lean

deleted theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits

deleted theorem IntermediateField.Lifts.exists_lift_of_splits'

deleted theorem IntermediateField.Lifts.exists_lift_of_splits

deleted theorem IntermediateField.Lifts.exists_upper_bound

deleted structure IntermediateField.Lifts

deleted theorem IntermediateField.exists_algHom_adjoin_of_splits'

deleted theorem IntermediateField.exists_algHom_adjoin_of_splits

deleted theorem IntermediateField.exists_algHom_adjoin_of_splits_of_aeval

deleted theorem IntermediateField.exists_algHom_of_adjoin_splits'

deleted theorem IntermediateField.exists_algHom_of_adjoin_splits

deleted theorem IntermediateField.exists_algHom_of_adjoin_splits_of_aeval

deleted theorem IntermediateField.exists_algHom_of_splits'

deleted theorem IntermediateField.exists_algHom_of_splits

deleted theorem IntermediateField.exists_algHom_of_splits_of_aeval

deleted theorem IntermediateField.nonempty_algHom_adjoin_of_splits

deleted theorem IntermediateField.nonempty_algHom_of_adjoin_splits

deleted theorem IntermediateField.nonempty_algHom_of_splits

Created Mathlib/FieldTheory/Extension.lean

added theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits

added theorem IntermediateField.Lifts.exists_lift_of_splits'

added theorem IntermediateField.Lifts.exists_lift_of_splits

added theorem IntermediateField.Lifts.exists_upper_bound

added structure IntermediateField.Lifts

added theorem IntermediateField.exists_algHom_adjoin_of_splits'

added theorem IntermediateField.exists_algHom_adjoin_of_splits

added theorem IntermediateField.exists_algHom_adjoin_of_splits_of_aeval

added theorem IntermediateField.exists_algHom_of_adjoin_splits'

added theorem IntermediateField.exists_algHom_of_adjoin_splits

added theorem IntermediateField.exists_algHom_of_adjoin_splits_of_aeval

added theorem IntermediateField.exists_algHom_of_splits'

added theorem IntermediateField.exists_algHom_of_splits

added theorem IntermediateField.exists_algHom_of_splits_of_aeval

added theorem IntermediateField.nonempty_algHom_adjoin_of_splits

added theorem IntermediateField.nonempty_algHom_of_adjoin_splits

added theorem IntermediateField.nonempty_algHom_of_splits

Modified Mathlib/FieldTheory/Normal.lean