restrictNormal' — Mathlib

English

There exists an algebra isomorphism on E obtained by restricting an isomorphism between K1 and K2 to the normal subfield, yielding an automorphism of E.

Русский

Существуют изоморфизм E ≃ₐ[F] E, получаемый ограничением изоморфизма между K1 и K2 к нормальному подполью.

LaTeX

$$$\text{RestrictNormal'}[\text{Normal } F E]\;: E \cong_{F} E,$$$

Lean4

/-- Restrict algebra homomorphism to normal subfield (`AlgEquiv` version) -/
def restrictNormal' [Normal F E] : E ≃ₐ[F] E :=
  AlgEquiv.ofBijective (AlgHom.restrictNormal ϕ E) (AlgHom.normal_bijective F E E _)

Похожие утверждения