irreducible_iff_irreducible_map_cast

English

Gauss's Lemma specialized to integers: for p ∈ Z[X], p.IsPrimitive implies Irreducible p iff Irreducible (p.map Int.castRingHom ℚ).

Русский

Специализация леммы Гаусса к целым: для p ∈ Z[X], если p примитивен, то p неприводим тогда и только тогда, когда p.map Int.castRingHom ℚ неприводим.

LaTeX

$$p.IsPrimitive → (Irreducible p ↔ Irreducible (p.map (Int.castRingHom ℚ)))$$

Lean4

/-- **Gauss's Lemma** for `ℤ` states that a primitive integer polynomial is irreducible iff it is
  irreducible over `ℚ`. -/
theorem irreducible_iff_irreducible_map_cast {p : ℤ[X]} (hp : p.IsPrimitive) :
    Irreducible p ↔ Irreducible (p.map (Int.castRingHom ℚ)) :=
  hp.irreducible_iff_irreducible_map_fraction_map

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