English
If R is a nontrivial ring, the polynomial ring R[X] is not finite as an R-module; equivalently, over a field this means R[X] is infinite-dimensional over R.
Русский
Если R не тривиально, то R[X] не конечен как модуль над R; то есть при полях R[X] является бесконечно-размерным векторным пространством над R.
LaTeX
$$$[\text{Nontrivial } R] \; \Rightarrow \; \lnot (\text{Module.Finite } R (R[X])).$$$
Lean4
/-- 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`. -/
theorem not_finite [Nontrivial R] : ¬Module.Finite R R[X] :=
by
rw [Module.finite_def, Submodule.fg_def]
push_neg
intro s hs contra
rcases span_le_degreeLE_of_finite hs with ⟨n, hn⟩
have : ((X : R[X]) ^ (n + 1)) ∈ Polynomial.degreeLE R ↑n :=
by
rw [contra] at hn
exact hn Submodule.mem_top
rw [mem_degreeLE, degree_X_pow, Nat.cast_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this
exact one_ne_zero this
