count_map_roots_of_injective — Mathlib

English

If p ∈ A[x], f : A →+* B is injective and p.map f ≠ 0, then the count inequality holds for all b ∈ B as in count_map_roots.

Русский

Если p ∈ A[x], f: A →+* B инъективен и p.map f ≠ 0, то неравенство счёта сохраняется для всех b ∈ B как в count_map_roots.

LaTeX

$$(count_map_roots_of_injective) — аналогичное утверждение для инъективного отображения$$

Lean4

theorem count_map_roots_of_injective [IsDomain A] [DecidableEq B] (p : A[X]) {f : A →+* B} (hf : Function.Injective f)
    (b : B) : (p.roots.map f).count b ≤ rootMultiplicity b (p.map f) :=
  by
  by_cases hp0 : p = 0
  ·
    simp only [hp0, roots_zero, Multiset.map_zero, Multiset.count_zero, Polynomial.map_zero, rootMultiplicity_zero,
      le_refl]
  · exact count_map_roots ((Polynomial.map_ne_zero_iff hf).mpr hp0) b

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