Commit 2025-01-10 01:57 2d57ce73

View on Github →

refactor: Split FieldTheory/Adjoin.lean into Defs.lean and Basic.lean (#20333) The file FieldTheory/Adjoin.lean was getting rather long, so I've split it into Defs.lean (importing only FieldTheory/IntermediateField/Basic.lean) and Basic.lean (everything else).

Estimated changes

deleted theorem AlgHom.fieldRange_eq_map
deleted theorem AlgHom.fieldRange_eq_top
deleted theorem AlgHom.map_fieldRange
deleted theorem IntermediateField.coe_bot
deleted theorem IntermediateField.coe_inf
deleted theorem IntermediateField.coe_top
deleted theorem IntermediateField.fg_bot
deleted theorem IntermediateField.fg_def
deleted theorem IntermediateField.fg_iSup
deleted theorem IntermediateField.fg_sup
deleted theorem IntermediateField.gc
deleted theorem IntermediateField.map_bot
deleted theorem IntermediateField.map_inf
deleted theorem IntermediateField.map_sup
deleted theorem IntermediateField.mem_bot
deleted theorem IntermediateField.mem_inf
deleted theorem IntermediateField.mem_top
deleted theorem IntermediateField.sup_def
added theorem AlgHom.map_fieldRange
added theorem IntermediateField.gc