finiteMultiplicity_X_sub_C — Mathlib

English

For any a ∈ R and nonzero p, the multiplicity of the factor X − C a in p is finite.

Русский

Для любого a ∈ R и ненулевого p конечна кратность делимости на (X − C a) в p.

LaTeX

$$$$ \\text{FiniteMultiplicity}\\big( X - C a\\big)\\, p. $$$$

Lean4

theorem finiteMultiplicity_X_sub_C (a : R) (h0 : p ≠ 0) : FiniteMultiplicity (X - C a) p :=
  by
  haveI := Nontrivial.of_polynomial_ne h0
  refine finiteMultiplicity_of_degree_pos_of_monic ?_ (monic_X_sub_C _) h0
  rw [degree_X_sub_C]
  decide
    /- TODO: stripping out classical for decidability instance parameter might
    make for better ergonomics -/

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