count_roots — Mathlib

English

The membership relation for roots: a ∈ p.roots iff p ≠ 0 ∧ IsRoot p a.

Русский

Членство a ∈ p.roots эквивалентно p ≠ 0 ∧ IsRoot p a.

LaTeX

$$a ∈ p.roots \iff p ≠ 0 ∧ IsRoot p a.$$

Lean4

@[simp]
theorem count_roots [DecidableEq R] (p : R[X]) : p.roots.count a = rootMultiplicity a p := by
  classical
  by_cases hp : p = 0
  · simp [hp]
  rw [roots_def, dif_neg hp]
  exact (Classical.choose_spec (exists_multiset_roots hp)).2 a

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