dvd_iff_fraction_map_dvd_fraction_map

English

For monic p, q ∈ R[X], p is a divisor of q in R[X] if and only if p.map(algebraMap R K) divides q.map(algebraMap R K) in K[X].

Русский

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

LaTeX

$$$p.Monic \\to q.Monic \\Rightarrow (q.map(\\mathrm{algebraMap } R K) \\mid p.map(\\mathrm{algebraMap } R K) \\iff q \\mid p)$$$

Lean4

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

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