Commit 2023-10-27 17:59 09820a53

View on Github →

fix(FieldTheory): add the missing _root_ lost during porting (#7981) You can tell this was a porting error because the #aligns were weird.

Estimated changes

Modified Mathlib/FieldTheory/Adjoin.lean

added theorem AlgEquiv.fieldRange_eq_top

added theorem AlgHom.fieldRange_eq_map

added theorem AlgHom.fieldRange_eq_top

added theorem AlgHom.map_fieldRange

deleted theorem IntermediateField.AlgEquiv.fieldRange_eq_top

deleted theorem IntermediateField.AlgHom.fieldRange_eq_map

deleted theorem IntermediateField.AlgHom.fieldRange_eq_top

deleted theorem IntermediateField.AlgHom.map_fieldRange

Modified Mathlib/FieldTheory/Normal.lean