Commit 2026-04-13 15:12 fa6418a8

feat(FieldTheory/IntermediateField): define the image of an intermediate field in a larger extension (#36772) Given a tower of fields K ⊆ L ⊆ M and an intermediate field F of L/K, defines IntermediateField.extendTop F M as the image of F under L →ₐ[K] M, together with instances transferring Algebra, IsFractionRing and IsIntegralClosure to the image. The main motivation is to embed a subextension F/K of L/K into a larger extension M/K. This is useful for instance when one needs M/K to be Galois. This construction will be useful in a later PR to prove that the compositum of two unramified extensions is unramified. Indeed, the result is first proved when the two extensions are IntermediateField K L with L/K Galois, and then in the general case (see #36843)