mod_coe_eq_self — Mathlib

English

For polynomials r with deg r less than the order, mod r.toPowerSeries equals r.

Русский

Для многочленов r с deg r < n, mod r.toPowerSeries = r.

LaTeX

$$$ [IsAdicComplete I A] \\Rightarrow \\mathrm{mod}(r^{\\!\!\\!\\!}) = r $$$

Lean4

theorem mod_coe_eq_self [IsAdicComplete I A] {r : A[X]} (hr : r.degree < (g.map (Ideal.Quotient.mk I)).order.toNat) :
    H.mod r = r := 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)).2

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