English
Equivalence equality for finSuccEquiv under a base algebra structure with a transitive chain of equalities.
Русский
Эквивалентность равенств для finSuccEquiv при основании над алгеброй с переходами равенств.
LaTeX
$$$\\text{Eq}(\\operatorname{finSuccEquiv} \\; R \\; n, \\ldots)$$$
Lean4
theorem support_finSuccEquiv (f : MvPolynomial (Fin (n + 1)) R) :
(finSuccEquiv R n f).support = Finset.image (fun m : Fin (n + 1) →₀ ℕ => m 0) f.support :=
by
ext i
rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff]
constructor
· rintro ⟨m, hm⟩
refine ⟨cons i m, ?_, cons_zero _ _⟩
rw [← support_coeff_finSuccEquiv]
simpa using hm
· rintro ⟨m, h, rfl⟩
refine ⟨tail m, ?_⟩
rwa [← coeff, zero_apply, ← mem_support_iff, support_coeff_finSuccEquiv, cons_tail]
