instIsScalarTowerSplittingField — Mathlib

English

Let F be a field, p ∈ F[X], E a field with an F-algebra structure such that p splits over E. Then the natural tower F → p.SplittingField → E forms a scalar tower (the scalar multiplications commute).

Русский

Пусть F – поле, p ∈ F[X], E – тело с F-алгеброй и предположим, что p распадается над E. Тогда цепь полей F ⊆ p.SplittingField ⊆ E образует цепь скаляров, то есть скаляры F корректно компонуются по секциям через p.SplittingField и E.

LaTeX

$$$\\operatorname{IsScalarTower}(F,\\; p.SplittingField,\\; E)$$$

Lean4

instance [h : Fact (p.Splits (algebraMap F E))] : IsScalarTower F p.SplittingField E :=
  IsScalarTower.of_algebraMap_eq fun x => ((IsSplittingField.lift p.SplittingField p h.1).commutes x).symm

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