liftNormal_commutes — Mathlib

English

The SplittingField construction is compatible with the Normal property, i.e., SplittingField carries a natural Normal structure.

Русский

Конструкция SplittingField совместима с нормальностью: она естественным образом носит структуру Normal.

LaTeX

$$Normal F p.SplittingField$$

Lean4

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

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