support_scaleRoots_eq — Mathlib

English

If s is a non-zero-divisor in R, then scaleRoots(p, s) has exactly the same support as p.

Русский

Если s не является делителем нуля в R, то поддержка scaleRoots(p, s) совпадает с поддержкой p.

LaTeX

$$$\text{(\}s \in \mathrm{nonZeroDivisors}(R)\text{\,)} \Rightarrow (\operatorname{support}(\operatorname{scaleRoots}(p, s)) = \operatorname{support}(p))$$$

Lean4

theorem support_scaleRoots_eq (p : R[X]) {s : R} (hs : s ∈ nonZeroDivisors R) : (scaleRoots p s).support = p.support :=
  le_antisymm (support_scaleRoots_le p s)
    (by
      intro i
      simp only [coeff_scaleRoots, Polynomial.mem_support_iff]
      intro p_ne_zero ps_zero
      have := (pow_mem hs (p.natDegree - i)).2 _ ps_zero
      contradiction)

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