eval — Mathlib

English

If x ≡ y mod I, then f.eval(x) ≡ f.eval(y) mod I for any polynomial f.

Русский

Если x ≡ y mod I, тогда f(x) ≡ f(y) mod I для любого многочлена f.

LaTeX

$$$$ x \\equiv y\\ [SMOD\\ I] \\Rightarrow \\forall f \\in \\mathbb{R}[X],\\ f.eval\\ x \\equiv f.eval\\ y\\ [SMOD\\ I]. $$$$

Lean4

@[gcongr]
theorem eval {R : Type*} [CommRing R] {I : Ideal R} {x y : R} (h : x ≡ y [SMOD I]) (f : R[X]) :
    f.eval x ≡ f.eval y [SMOD I] :=
  by
  simp_rw [Polynomial.eval_eq_sum, Polynomial.sum]
  gcongr

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