English
restrictDvd encodes restriction maps for divisibility relations between polynomials, giving a monoid hom from the Galois group of q to that of p when p divides q.
Русский
restrictDvd кодирует отображения ограничения для отношения делимости между многочленами, образуя моноид-гомоморф от Gal(q) к Gal(p), если p ∣ q.
LaTeX
$${F : Type} → [Field F] → {p q : Polynomial F} → semigroupDvd.dvd p q → MonoidHom q.Gal p.Gal$$
Lean4
/-- `Polynomial.Gal.restrict`, when both fields are splitting fields of polynomials. -/
def restrictDvd (hpq : p ∣ q) : q.Gal →* p.Gal :=
haveI := Classical.dec (q = 0)
if hq : q = 0 then 1
else @restrict F _ p _ _ _ ⟨splits_of_splits_of_dvd (algebraMap F q.SplittingField) hq (SplittingField.splits q) hpq⟩
