div_coe_eq_zero — Mathlib

English

If g q + r = g q' + r' with deg r, deg r' < n, then q = q' and r = r'.

Русский

Если g q + r = g q' + r' при deg r, deg r' < n, то q = q' и r = r'.

LaTeX

$$$ gq + r = gq' + r' \\land \\deg(r)

Lean4

theorem div_coe_eq_zero [IsAdicComplete I A] {r : A[X]} (hr : r.degree < (g.map (Ideal.Quotient.mk I)).order.toNat) :
    H.div r = 0 := by
  obtain ⟨h1, h2⟩ := H.isWeierstrassDivisionAt_div_mod r
  exact (H.eq_of_mul_add_eq_mul_add (q := H.div r) (q' := 0) h1 hr (by simpa using h2.symm)).1

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