zero_notMem_multiset_map_X_sub_C — Mathlib

English

For any multiset m of indices and function f, the image under mapping a ↦ X − C(f(a)) of m does not contain the zero polynomial.

Русский

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

LaTeX

$$$(0) \notin m\mapsto (\,X - C(f(a))\,)$.$$

Lean4

theorem zero_notMem_multiset_map_X_sub_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_sub_C_ne_zero _ ha

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