support_coeff_finSuccEquiv — Mathlib

English

For any p, the membership of an index i in the support of optionEquivLeft(R,S1)(p) matches the membership of i in the degree structure of p.

Русский

Для любого p верно равенство членства i в опорe optionEquivLeft(p) и членство i в структуре степеней p.

LaTeX

$$$\\operatorname{natDegree}(((\\operatorname{optionEquivLeft} R S_1\\;p).\\coeff i)) = \\text{…}$$$

Lean4

theorem support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {m : Fin n →₀ ℕ} :
    m ∈ ((finSuccEquiv R n f).coeff i).support ↔ m.cons i ∈ f.support :=
  by
  apply Iff.intro
  · intro h
    simpa [← finSuccEquiv_coeff_coeff] using h
  · intro h
    simpa [mem_support_iff, ← finSuccEquiv_coeff_coeff m f i] using h

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