restrictNormal_commutes — Mathlib

English

Restriction to a normal subfield yields an automorphism of the subfield’s automorphism group, forming a homomorphism from automorphisms to automorphisms.

Русский

Ограничение к нормальному подполя образует автоморфизм группы автоморфизмов подполя, образуя гомоморфизм между группами

LaTeX

$$$\text{restrictNormalHom }[Normal F E] : (K_1 \cong_F K_2) \to (E \cong_F E)$$$

Lean4

@[simp]
theorem restrictNormal_commutes [Normal F E] (x : E) : algebraMap E K₂ (χ.restrictNormal E x) = χ (algebraMap E K₁ x) :=
  χ.toAlgHom.restrictNormal_commutes E x

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