Commit 2024-11-07 05:00 47beff8a

View on Github →

feat(FieldTheory): new Adjoin lemmas and finish up #17543 (#18430)

Estimated changes

Modified Mathlib/Algebra/Field/Subfield.lean

modified theorem Subfield.closure_induction

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem IntermediateField.adjoin_algHom_ext

added theorem IntermediateField.adjoin_iUnion

modified theorem IntermediateField.adjoin_induction

added theorem IntermediateField.adjoin_union

added theorem IntermediateField.algHom_ext_of_eq_adjoin

deleted theorem IntermediateField.fG_of_fG_toSubalgebra

added theorem IntermediateField.fg_adjoin_of_finite

added theorem IntermediateField.fg_iSup

added theorem IntermediateField.fg_of_fg_toSubalgebra

added theorem IntermediateField.fg_sup

added theorem IntermediateField.iSup_eq_adjoin

added theorem IntermediateField.restrictScalars_adjoin_eq_sup