# Zulip Chat Archive

## 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}$.

#### Kenny Lau (Nov 27 2020 at 15:37):

@Patrick Lutz @Simon Andreys docs#adjoin_root.power_basis

#### 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_polynomial`

s 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