restrict_surjective — Mathlib

English

If p splits over E and E is normal over F, then the restriction map restrict p E is surjective onto p.Gal.

Русский

Если p распадается над E и E является нормальным над F, то отображение ограничения на p.Gal плотно отображает все элементы p.Gal; то есть ограничение достижимо на всю галловскую группу p.

LaTeX

$$$\\operatorname{Surjective}(\\operatorname{restrict}(p,E))$$$

Lean4

theorem restrict_surjective [Fact (p.Splits (algebraMap F E))] [Normal F E] : Function.Surjective (restrict p E) :=
  AlgEquiv.restrictNormalHom_surjective E

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