rootMultiplicity_eq_multiplicity — Mathlib

English

For any p and a, rootMultiplicity a p equals 0 if p = 0; otherwise it equals the multiplicity of X − C a in p.

Русский

Для любого p и a, rootMultiplicity a p равно 0, если p = 0; иначе — кратность (X − C a) в p.

LaTeX

$$$$ \\operatorname{rootMultiplicity}(a, p) = \\begin{cases} 0, & p = 0, \\\\ \\operatorname{multiplicity}(X - C a, p), & p \\neq 0. \\end{cases} $$$$

Lean4

theorem rootMultiplicity_eq_multiplicity [DecidableEq R] (p : R[X]) (a : R) :
    rootMultiplicity a p = if p = 0 then 0 else multiplicity (X - C a) p :=
  by
  simp only [rootMultiplicity, multiplicity, emultiplicity]
  split
  · rfl
  rename_i h
  simp only [finiteMultiplicity_X_sub_C a h, ↓reduceDIte]
  rw [← ENat.some_eq_coe, WithTop.untopD_coe]
  congr

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