dvd_iff_fraction_map_dvd_fraction_map

English

For primitive p, q, p divides q in R[X] if and only if p.map(algebraMap R K) divides q.map(algebraMap R K) in K[X].

Русский

Для примитивных p, q: p делит q в R[X] тогда и только тогда, когда p.map(algebraMap R K) делит q.map(algebraMap R K) в K[X].

LaTeX

$$p.IsPrimitive → q.IsPrimitive → (p ∣ q ↔ p.map(\\mathrm{algebraMap} R K) ∣ q.map(\\mathrm{algebraMap} R K))$$

Lean4

theorem dvd_iff_fraction_map_dvd_fraction_map {p q : R[X]} (hp : p.IsPrimitive) (hq : q.IsPrimitive) :
    p ∣ q ↔ p.map (algebraMap R K) ∣ q.map (algebraMap R K) :=
  ⟨fun ⟨a, b⟩ => ⟨a.map (algebraMap R K), b.symm ▸ Polynomial.map_mul (algebraMap R K)⟩, fun h =>
    hp.dvd_of_fraction_map_dvd_fraction_map hq h⟩

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