Theorems · Theorem · commutative algebra

Polynomial.not_finite

∀ {R : Type u} [inst : Semiring R] [Nontrivial R], ¬Module.Finite R (Polynomial R)

If R is a nontrivial ring, the polynomials R[X] are not finite as an R-module. When R is a field, this is equivalent to R[X] being an infinite-dimensional vector space over R.

Defined in

Mathlib.RingTheory.Polynomial.Basic

Cited by

1 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringNontrivial