English
A monic polynomial in the free polynomial ring on Fin(n+1) variables, with a distinguished last variable X, together with the non-leading coefficients indexed by Fin n.
Русский
Монический многочлен в свободной кольцевой паре на Fin(n+1) переменных, где последняя переменная обозначает X, а остальные — нен leading коэффициенты.
LaTeX
$$genericMonicPoly(n) : FreeCommRing (Fin(n+1)) := of (Fin.last _)^n + ∑ i : Fin n, of i.castSucc * of (Fin.last _)^(i)$$
Lean4
/-- A generic monic polynomial of degree `n` as an element of the
free commutative ring in `n + 1` variables, with a variable for each
of the `n` non-leading coefficients of the polynomial and one variable (`Fin.last n`)
for `X`. -/
def genericMonicPoly (n : ℕ) : FreeCommRing (Fin (n + 1)) :=
of (Fin.last _) ^ n + ∑ i : Fin n, of i.castSucc * of (Fin.last _) ^ (i : ℕ)
