mem_image_support_coeff_finSuccEquiv

English

The i-th coefficient's support under finSuccEquiv corresponds to the coefficient's support of f at m.cons i.

Русский

Опора i-го коэффициента через finSuccEquiv соответствует опоре коэффициента f в m.cons i.

LaTeX

$$$\\text{coeff}_{(\\operatorname{Fin}(n)\\to 0)^{}}(\\operatorname{finSuccEquiv} \\; R \\; n \\; f) = \\ldots$$$

Lean4

theorem mem_image_support_coeff_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x} :
    x ∈ Finsupp.cons i '' ((finSuccEquiv R n f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i := by
  simpa using congr(x ∈ $image_support_finSuccEquiv)

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