rootMultiplicity_eq_rootMultiplicity

English

The multiplicity of t as a root of p equals the multiplicity of 0 as a root of p ∘ (X + C t).

Русский

Кратность t как корня p равна кратности 0 как корня композиции p ∘ (X + C t).

LaTeX

$$$$ \\operatorname{rootMultiplicity} t\\, p = \\operatorname{rootMultiplicity} 0\\, \\big(p \\circ (X + C t)\\big). $$$$

Lean4

theorem rootMultiplicity_eq_rootMultiplicity {p : R[X]} {t : R} :
    p.rootMultiplicity t = (p.comp (X + C t)).rootMultiplicity 0 := by
  classical
  simp_rw [rootMultiplicity_eq_multiplicity, comp_X_add_C_eq_zero_iff]
  congr 1
  rw [C_0, sub_zero]
  convert (multiplicity_map_eq <| algEquivAevalXAddC t).symm using 2
  simp [C_eq_algebraMap]

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