image_support_finSuccEquiv — Mathlib

English

The support of finSuccEquiv(R,n) f coincides with the image of the first coordinate 0 of the finsupp supporting f.

Русский

Опора финSuccEquiv совпадает с образом нулевой координаты опорного множества f.

LaTeX

$$$\\mathrm{support}(\\operatorname{finSuccEquiv} R n \\; f) = \\mathrm{image}\\bigl(\\lambda m. m\\,0\\bigr)\\; f.support$$$

Lean4

theorem image_support_finSuccEquiv {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} :
    ((finSuccEquiv R n f).coeff i).support.image (Finsupp.cons i) = {m ∈ f.support | m 0 = i} :=
  by
  ext m
  rw [Finset.mem_filter, Finset.mem_image, mem_support_iff]
  conv_lhs =>
    congr
    ext
    rw [mem_support_iff, finSuccEquiv_coeff_coeff, Ne]
  constructor
  · grind [cons_zero]
  · intro h
    use tail m
    rw [← h.2, cons_tail]
    simp [h.1]

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