English
The finSuccEquiv is equal to the composition of renameEquiv and optionEquivLeft, i.e., finSuccEquiv = renameEquiv ∘ optionEquivLeft.
Русский
finSuccEquiv равен композиции renameEquiv и optionEquivLeft, то есть finSuccEquiv = renameEquiv ∘ optionEquivLeft.
LaTeX
$$$\\operatorname{finSuccEquiv} \\; R\\; n = (\\operatorname{renameEquiv} R (\\operatorname{finSuccEquiv} n)) \\circ (\\operatorname{optionEquivLeft} R (\\operatorname{Fin} n))$$$
Lean4
theorem finSuccEquiv_eq :
(finSuccEquiv R n : MvPolynomial (Fin (n + 1)) R →+* Polynomial (MvPolynomial (Fin n) R)) =
eval₂Hom (Polynomial.C.comp (C : R →+* MvPolynomial (Fin n) R)) fun i : Fin (n + 1) =>
Fin.cases Polynomial.X (fun k => Polynomial.C (X k)) i :=
by
ext i : 2
· simp only [finSuccEquiv, optionEquivLeft_apply, aeval_C, AlgEquiv.coe_trans, RingHom.coe_coe, coe_eval₂Hom,
comp_apply, renameEquiv_apply, eval₂_C, RingHom.coe_comp, rename_C]
rfl
· refine Fin.cases ?_ ?_ i <;> simp [optionEquivLeft_apply, finSuccEquiv]
