dvd_iff_map_cast_dvd_map_cast — Mathlib

English

For p, q ∈ Z[X], p.IsPrimitive and q.IsPrimitive, p divides q in Z[X] if and only if p.map(Int.castRingHom ℚ) divides q.map(Int.castRingHom ℚ) in Q[X].

Русский

Для p, q ∈ Z[X], если p и q примитивны, то p делит q в Z[X] тогда и только тогда, когда p.map Int.castRingHom ℚ делит q.map Int.castRingHom ℚ в Q[X].

LaTeX

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

Lean4

theorem dvd_iff_map_cast_dvd_map_cast (p q : ℤ[X]) (hp : p.IsPrimitive) (hq : q.IsPrimitive) :
    p ∣ q ↔ p.map (Int.castRingHom ℚ) ∣ q.map (Int.castRingHom ℚ) :=
  hp.dvd_iff_fraction_map_dvd_fraction_map ℚ hq

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