support_restriction — Mathlib

English

Let p be a polynomial with coefficients in a ring R. Restricting p to a subring (via a suitable restriction operation) does not change the set of indices where its coefficients are nonzero.

Русский

Пусть p — многочлен над кольцом R. Ограничение коэффициентов до подкольца не изменяет множество индексов ненулевых коэффициентов.

LaTeX

$$$\\operatorname{supp}(\\mathrm{restriction}(p)) = \\operatorname{supp}(p)$$$

Lean4

@[simp]
theorem support_restriction (p : R[X]) : support (restriction p) = support p :=
  by
  ext i
  simp only [mem_support_iff, not_iff_not, Ne]
  conv_rhs => rw [← coeff_restriction]
  exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩

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