mem_support_coeff_finSuccEquiv — Mathlib

English

For any j in Fin n, finSuccEquiv(R n)(X j.succ) equals C(X j).

Русский

Для каждого j ∈ Fin n, финSuccEquiv(R,n)(X j.succ) равно C(X j).

LaTeX

$$$\\forall j : \\mathrm{Fin}(n), \\; \\operatorname{finSuccEquiv} \\; R \\; n (X j.succ) = \\operatorname{Polynomial}.C( X j )$$$

Lean4

theorem mem_support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
    x ∈ ((finSuccEquiv R n f).coeff i).support ↔ x.cons i ∈ f.support :=
  by
  rw [← (Finsupp.cons_right_injective i).mem_finset_image (a := x), image_support_finSuccEquiv]
  simp only [Finset.mem_filter, mem_support_iff, ne_eq, cons_zero, and_true]
    -- TODO: generalize `finSuccEquiv R n` to an arbitrary ZeroHom

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