English
For a commutative ring K and nontrivial K, the lift of the generic monic polynomial equals its evaluation via a degree-tracking equivalence, relating FreeCommRing.lift to a polynomial evaluation.
Русский
Для коммутативного кольца K и ненулевого K, лифт-образ общего монического полинома равен его оценке через эквивалентности степеней, связывая FreeCommRing.lift и оценку полинома.
LaTeX
$$lift v (genericMonicPoly n) = (((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc)).1.eval (v (Fin.last _))$$
Lean4
theorem lift_genericMonicPoly [CommRing K] [Nontrivial K] {n : ℕ} (v : Fin (n + 1) → K) :
FreeCommRing.lift v (genericMonicPoly n) =
(((monicEquivDegreeLT n).trans (degreeLTEquiv K n).toEquiv).symm (v ∘ Fin.castSucc)).1.eval (v (Fin.last _)) :=
by simp [genericMonicPoly, monicEquivDegreeLT, degreeLTEquiv, eval_finset_sum]
