modByMonic_eq_zero_iff_quotient_eq_zero

English

For polynomials p and monic q, p mod q is zero iff p is divisible by q in the polynomial ring modulo I.

Русский

Для полиномов p и монотического q, остаток от деления p на q равен нулю тогда и только тогда, когда p делится на q в кольце полиномов по И.

LaTeX

$$$\\forall p,q\\, (q\\text{ monic}):\\, p \\,\\%_m \\, q = 0 \\iff (p : R[X] / (q)) = 0$$$

Lean4

theorem modByMonic_eq_zero_iff_quotient_eq_zero (p q : R[X]) (hq : q.Monic) :
    p %ₘ q = 0 ↔ (p : R[X] ⧸ Ideal.span { q }) = 0 := by
  rw [modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]

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