coeffIntegerNormalization_mem_support

English

If coeffIntegerNormalization M p i ≠ 0, then i ∈ the support of p.

Русский

Если коэффициент нормализации i не равен нулю, то i принадлежит поддержке p.

LaTeX

$$$\text{coeffIntegerNormalization }(M,p,i) \neq 0 \Rightarrow i \in \mathrm{support}(p)$$$

Lean4

theorem coeffIntegerNormalization_mem_support (p : S[X]) (i : ℕ) (h : coeffIntegerNormalization M p i ≠ 0) :
    i ∈ p.support := by
  contrapose h
  rw [Ne, Classical.not_not, coeffIntegerNormalization, dif_neg h]

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