instAlgebraSplittingFieldOfFactSplitsAlgebraMap

English

If p splits over F and maps into E via an algebra map, then there is a natural Algebra structure on p.SplittingField E.

Русский

Если p splits над F и задан алгебраическим отображением в E, то на p.SplittingField E существует естественная структура Algebra.

LaTeX

$$$[h:\ Fact(Polynomials.Splits (algebraMap F E) p)] \Rightarrow Algebra p.SplittingField E$$$

Lean4

instance [h : Fact (p.Splits (algebraMap F E))] : Algebra p.SplittingField E :=
  (IsSplittingField.lift p.SplittingField p h.1).toRingHom.toAlgebra

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