一元有理係數多項式

數學敘述

Q[x] 的一元多項式以有限個有理係數 a_k 表示 p(x)=a_0+a_1x+⋯+a_nx^n，指數均為非負整數。非零多項式的次數為最大非零係數的索引；本條目把零多項式的次數記為未定義。

代表公式（精確 TeX）

x^{n}

成立條件

• 固定形式變數 x，係數屬於 Q，僅有限個係數非零。
• 係數向量按 [a_0,a_1,…] 由低次至高次排列；尾端零不改變多項式。

符號作用域

• x — 形式變數
• n — 代表單項式的非負整數指數

直觀、定義與常見誤解

多項式不是只看字面項數。相同次冪的係數要先相加；例如 x²−x²+3 化成常數 3，次數為零。零多項式與非零常數多項式不可混淆。

加法逐次相加係數；乘法按指數和合併，所得係數是有限卷積。代入一個數值是對同一份係數資料求值，單個代入值相等不建立多項式恆等式。

本輪題庫限定整數係數與整數輸入的精確切片，係數查詢超過支撐處為零。零多項式的『未定義』是教學慣例；未來須分別對應 Mathlib.degree 的 ⊥ 與 natDegree 的補零，不能混作一般次數。

未先合併同次項就取最高字面指數，或用向量長度及尾端零決定次數。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 變數與代數式 — 先區分形式表達式與指定代入值。
• 自然數冪與主平方根 — 多項式項使用非負整數次冪。
• 有理數 — 係數明示在有理數域中。

驗證界線

有限係數可逐項驗證；本條目尚未形式化多項式資料、求值與次數的語義橋。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。

下一個義務

綁定 Polynomial Q、coeff、eval、degree 與 natDegree 的零多項式差異。

同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。