exists_eq_pow_rootMultiplicity_mul_and_not_dvd

English

For p ≠ 0, there exists q such that p = (X - C a)^{rootMultiplicity a p} · q and (X - C a) ∤ q.

Русский

Для p ≠ 0 существует q, такое что p = (X − C a)^{rootMultiplicity a p} · q и (X − C a) не делит q.

LaTeX

$$$$ \\exists q \\in R[X],\\; p = (X - C a)^{\\operatorname{rootMultiplicity} a p} \\cdot q \\land \\; (X - C a) \\nmid q. $$$$

Lean4

theorem exists_eq_pow_rootMultiplicity_mul_and_not_dvd (p : R[X]) (hp : p ≠ 0) (a : R) :
    ∃ q : R[X], p = (X - C a) ^ p.rootMultiplicity a * q ∧ ¬(X - C a) ∣ q := by
  classical
  rw [rootMultiplicity_eq_multiplicity, if_neg hp]
  apply (finiteMultiplicity_X_sub_C a hp).exists_eq_pow_mul_and_not_dvd

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