zero_notMem_multiset_map_X_add_C — Mathlib

English

For any multiset m and any function f, every polynomial of the form X + C(f(a)) is nonzero; consequently the zero polynomial does not appear in the multiset image m.map(a ↦ X + C(f(a))).

Русский

Для любой мультимножины m и любой функции f каждый многочлен вида X + C(f(a)) ненулевой; следовательно нулевой многочлен не принадлежит образу m под отображением a ↦ X + C(f(a)).

LaTeX

$$$0 \notin m.map\bigl(\lambda a. X + C (f a)\bigr)$$$

Lean4

theorem zero_notMem_multiset_map_X_add_C {α : Type*} (m : Multiset α) (f : α → R) :
    (0 : R[X]) ∉ m.map fun a => X + C (f a) := fun mem =>
  let ⟨_a, _, ha⟩ := Multiset.mem_map.mp mem
  X_add_C_ne_zero _ ha

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