English
Applying galRestrict to σ and x yields the same value as galRestrictHom.
Русский
Применение galRestrict к σ и x даёт такое же значение, как и galRestrictHom.
LaTeX
$$galRestrict_apply (σ : L ≃ₐ[K] L) (x : B) : galRestrict A K L B σ x = galRestrictHom A K L B σ x$$
Lean4
/-- The restriction `Aut(L/K) → Aut(B/A)` in an AKLB setup. -/
noncomputable def galRestrict : (L ≃ₐ[K] L) ≃* (B ≃ₐ[A] B) :=
(AlgEquiv.algHomUnitsEquiv K L).symm.trans
((Units.mapEquiv <| galRestrictHom A K L B).trans (AlgEquiv.algHomUnitsEquiv A B))