restrictProd — Mathlib

English

For polynomials p and q, the Galois group of p • q maps to the product of Gal(p) and Gal(q) via restrictDvd with the product structure.

Русский

Для многочленов p и q группа Гал(p·q) отображается в произведение Gal(p) × Gal(q) через restrictDvd с учётом произведения.

LaTeX

$$$\\mathrm{restrictProd} : (p*q).Gal \\to^* p.Gal \\times q.Gal$$$

Lean4

/-- The Galois group of a product maps into the product of the Galois groups. -/
def restrictProd : (p * q).Gal →* p.Gal × q.Gal :=
  MonoidHom.prod (restrictDvd (dvd_mul_right p q)) (restrictDvd (dvd_mul_left q p))

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