support_toSubring — Mathlib

English

The support of the subring-lifted polynomial matches the support of the original polynomial.

Русский

Опора полинома, полученного посредством toSubring, совпадает с опорой исходного полинома.

LaTeX

$$$\\operatorname{support}(\\mathrm{toSubring}\\ p\\ T\\ hp) = \\operatorname{support}(p)$$$

Lean4

@[simp]
theorem support_toSubring : support (toSubring p T hp) = support p :=
  by
  ext i
  simp only [mem_support_iff, not_iff_not, Ne]
  conv_rhs => rw [← coeff_toSubring p T hp]
  exact ⟨fun H => by rw [H, ZeroMemClass.coe_zero], fun H => Subtype.coe_injective H⟩

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