pow_mul_divByMonic_rootMultiplicity_eq

English

(X - C a)^{rootMultiplicity a p} divides p

Русский

(X − C a)^{rootMultiplicity a p} делит p

LaTeX

$$$$ (X - C a)^{\\operatorname{rootMultiplicity} a p} \\mid p. $$$$

Lean4

theorem pow_mul_divByMonic_rootMultiplicity_eq (p : R[X]) (a : R) :
    (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p :=
  by
  have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _
  conv_rhs => rw [← modByMonic_add_div p this, (modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]
  simp

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