Commit 2025-10-23 00:03 9fdf9114

View on Github →

feat(AdjoinRoot): bundle operations as AlgHoms (#29132) In particular, generalise and rename liftHom to use a general eval₂ instead of aeval. From Toric

Estimated changes

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Modified Mathlib/FieldTheory/Isaacs.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

Modified Mathlib/RingTheory/Adjoin/Field.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem AdjoinRoot.algHom_ext'

added theorem AdjoinRoot.coe_liftAlgHom

added theorem AdjoinRoot.coe_ofAlgHom

added def AdjoinRoot.liftAlgHom

added theorem AdjoinRoot.liftAlgHom_eq_algHom

added theorem AdjoinRoot.liftAlgHom_mk

added theorem AdjoinRoot.liftAlgHom_of

added theorem AdjoinRoot.liftAlgHom_root

modified theorem AdjoinRoot.liftHom_mk

added theorem AdjoinRoot.toRingHom_liftAlgHom

added theorem AdjoinRoot.toRingHom_ofAlgHom

modified def AdjoinRoot

Modified Mathlib/RingTheory/Localization/Away/AdjoinRoot.lean