rootMultiplicity_expand — Mathlib

English

The base case of expansion gives: rootMultiplicity(t, expand_R(p,f)) = p · rootMultiplicity(t^p, f).

Русский

База для расширения: кратность корня после раскрытия: rootMultiplicity(t, expand_R(p,f)) = p · rootMultiplicity(t^p, f).

LaTeX

$$$$\mathrm{rootMultiplicity}(t, \mathrm{expand}_R(p,f))=p\cdot \mathrm{rootMultiplicity}(t^p, f)$$$$

Lean4

theorem rootMultiplicity_expand : (expand R p f).rootMultiplicity r = p * f.rootMultiplicity (r ^ p) := by
  rw [← pow_one p, rootMultiplicity_expand_pow]

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