restrictComp — Mathlib

English

If q.natDegree ≠ 0, then restrictComp p q is surjective.

Русский

Если natDegree(q) ≠ 0, то restrictComp p q сюръективно.

LaTeX

$$$\\operatorname{Surjective}(\\mathrm{restrictComp}\\ p\\ q\\ hq)$$$

Lean4

/-- `Polynomial.Gal.restrict` for the composition of polynomials. -/
def restrictComp (hq : q.natDegree ≠ 0) : (p.comp q).Gal →* p.Gal :=
  let h : Fact (Splits (algebraMap F (p.comp q).SplittingField) p) := ⟨splits_in_splittingField_of_comp p q hq⟩
  @restrict F _ p _ _ _ h

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