aeval_modByMonic_eq_self_of_root — Mathlib

English

For any ring R, any a ∈ R and any n ∈ N, the root multiplicity of a as a root of (X − a)^n is n, provided R is suitable (nontrivial).

Русский

Для кольца R и элемента a ∈ R и целого n ≥ 0 мультипликатор корня корня a для (X − a)^n равен n (при подходящих условиях на R).

LaTeX

$$$$ \\operatorname{rootMultiplicity} a \\big( (X - C a)^n \\big) = n. $$$$

Lean4

theorem aeval_modByMonic_eq_self_of_root [Algebra R S] {p q : R[X]} (hq : q.Monic) {x : S} (hx : aeval x q = 0) :
    aeval x (p %ₘ q) = aeval x p := by
  --`eval₂_modByMonic_eq_self_of_root` doesn't work here as it needs commutativity
  rw [modByMonic_eq_sub_mul_div p hq, map_sub, map_mul, hx, zero_mul, sub_zero]

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