Basis for quotient of polynomial ring

Stream: Is there code for X?

[Patrick Lutz]

Is there anything already in mathlib proving that the dimension of $F[x]/p$ as a vector space over $F$ is the degree of $p$ (where $F$ is a field and $p$ is a nonzero polynomial over $F$) or that $1, x, \ldots, x^{n - 1}$ is a basis (where $n$ is the degree of $p$)?

[Simon Andreys]

I would be interested in that too ! I'd use the basis $1, (x-\lambda), ..., (x-\lambda)^{n-1}$.

[Kenny Lau]

@Patrick Lutz @Simon Andreys docs#adjoin_root.power_basis

[Simon Andreys]

Great thank you !

[Simon Andreys]

The terminology is a bit confusing here... adjoin_root only deserves its name when p is irreducible, but the definition and theorem do not require any proof that p is irreducible so it works fine anyway.

[Kevin Buzzard]

Definitions and theorems in Lean are intentially formalised so that they require the bare minimum from the inputs, just enough to make sense (for example the Sup function on the reals doesn't require the set to be nonempty or bounded above, and the square root function on the reals doesn't demand that the input is nonnegative). On the other hand I think $R[X]/(p(X))$ is in some sense the universal way of adjoining a root of $p$ to $R$.

[Simon Andreys]

Indeed, it was the math I was actually confused about, not the terminology ! I'm not used to consider polynomials on a ring which is not a field.

[Aaron Anderson]

Do we have a basis for the (mv_)polynomial ring itself?

[Aaron Anderson]

It wouldn't be a power_basis, because that assumes finiteness.

[Aaron Anderson]

I'd like to be able to define a linear_map from a polynomial ring, and one way to do that would be using is_basis.constr if we know the powers of X form a basis.

[Aaron Anderson]

(I'm sure other ways exist, but I'd still like to have that basis.)

[Kevin Buzzard]

My memory from working with mv_polynomials was that we do not have this. We have monomial s a which is $aX^{s}$ (here s : σ →₀ ℕ) and these span mv_polynomial R σ as an abelian group, which in my experience turned out to be good enough. You can of course use monomial s 1. Beware the zero ring.