rootMultiplicity_C — Mathlib

English

For any r and a, rootMultiplicity a (C r) = 0.

Русский

Для любых r, a: rootMultiplicity a (C r) = 0.

LaTeX

$$$$ \\operatorname{rootMultiplicity}(a, \\; C r) = 0. $$$$

Lean4

@[simp]
theorem rootMultiplicity_C (r a : R) : rootMultiplicity a (C r) = 0 :=
  by
  cases subsingleton_or_nontrivial R
  · rw [Subsingleton.elim (C r) 0, rootMultiplicity_zero]
  classical
  rw [rootMultiplicity_eq_multiplicity]
  split_ifs with hr
  · rfl
  have h : natDegree (C r) < natDegree (X - C a) := by simp
  simp_rw [multiplicity_eq_zero.mpr ((monic_X_sub_C a).not_dvd_of_natDegree_lt hr h)]

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