## Stream: Is there code for X?

### Topic: Basis for quotient of polynomial ring

#### Patrick Lutz (Sep 28 2020 at 18:30):

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 (Nov 27 2020 at 15:31):

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

#### Simon Andreys (Nov 27 2020 at 15:40):

Great thank you !

#### Simon Andreys (Nov 27 2020 at 17:59):

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 (Nov 27 2020 at 18:10):

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 (Nov 28 2020 at 10:42):

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 (Dec 04 2020 at 18:45):

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

#### Aaron Anderson (Dec 04 2020 at 18:46):

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

#### Aaron Anderson (Dec 04 2020 at 18:46):

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 (Dec 04 2020 at 18:47):

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

#### Kevin Buzzard (Dec 04 2020 at 19:07):

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.

Last updated: May 17 2021 at 15:13 UTC