Polynomial_Functions_form_Submodule_of_All_Functions

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

linear-algebramodulespolynomialsproofwiki

Let $K$ be a commutative ring with unity. Let $K^K$ be the $K$ -module mappings $f: K \to K$ . Let $P \left({K}\right) \subseteq K^K$ be the set of all polynomial functions on $K$ . Then $P \left({K}\right)$ is a $K$ -submodule of $K^K$ .

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.RingTheory.Polynomial.Basic

Formal statement

theorem Polynomial_Functions_form_Submodule_of_All_Functions {K : Type _} [CommRing K] : ∃ (S : Submodule K (K → K)), ∀ (p : Polynomial K), (fun x => Polynomial.eval x p) ∈ S := by sorry

Source

https://proofwiki.org/wiki/Polynomial_Functions_form_Submodule_of_All_Functions

View graph