instNormal

Mathlib.FieldTheory.Normal.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.SplittingField.instNormal

English

If E is a normal subfield of K over F and f: E →ₐ[F] K is an F-algebra homomorphism, then its fieldRange equals E.

Русский

Пусть E ⊆ K нормальное, и f: E →ₐ[F] K — алгебраHom над F; тогда fieldRange(f)=E.

LaTeX

$$$f.fieldRange = E$$$

Lean4

instance instNormal (p : F[X]) : Normal F p.SplittingField :=
  Normal.of_isSplittingField p

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru