English
The composition of the inverse finSuccEquiv with Polynomial.C composed with MvPolynomial.C equals MvPolynomial.C.
Русский
Композиция обратной фин succ эквив между Polynomial.C и MvPolynomial.C равна MvPolynomial.C.
LaTeX
$$$\\bigl(\\uparrow(\\operatorname{finSuccEquiv} R n).symm).comp(\\operatorname{Polynomial}.C.\\operatorname{comp} MvPolynomial.C) = \\operatorname{MvPolynomial.C}$$$
Lean4
theorem finSuccEquiv_comp_C_eq_C {R : Type u} [CommSemiring R] (n : ℕ) :
(↑(MvPolynomial.finSuccEquiv R n).symm : Polynomial (MvPolynomial (Fin n) R) →+* _).comp
(Polynomial.C.comp MvPolynomial.C) =
(MvPolynomial.C : R →+* MvPolynomial (Fin n.succ) R) :=
by
refine RingHom.ext fun x => ?_
rw [RingHom.comp_apply]
refine (MvPolynomial.finSuccEquiv R n).injective (Trans.trans ((MvPolynomial.finSuccEquiv R n).apply_symm_apply _) ?_)
simp only [MvPolynomial.finSuccEquiv_apply, MvPolynomial.eval₂Hom_C]
