有限域
有限交換含一環中每個非零元素皆有乘法逆元時構成有限域。
mko-finite-field · definition · v0.10.0
數學敘述
以完整有限環雙表核1不等於0、乘法交換及每個非零元素的雙側逆元。除法只對非零除數定義。有限整環成域是利用有限乘法映射單射推出滿射的定理步驟;域階為質數冪,不必是質數。
代表公式(精確 TeX)
F(R)
成立條件
- 完整有限交換含一環表及零、一明示。
- 逆元逐全部非零元素核對;永不除以零。
符號作用域
F— 有限域R— 父有限整環
直觀、定義與常見誤解
完整搜尋每個非零元逆元。
有限整環到域保留單射/滿射定理步驟。
有限域階可為p的冪,不限質數。
把任意有限交換環當域、允許除以零,或宣稱有限域階一定是質數。
已採用的推導導讀
完整表認證 F₃ 與有限整環引理原始 MKO 保留;導讀有自己的追加式修訂與驗證界線,不代表新 Lean 證明。
前置知識
驗證界線
只分類指定完整有限表;不外推任意交換環或省略非零逆元責任。
not_formalized
這不表示內容錯誤;只表示尚未登錄可重播的計算或形式證據。
下一個義務
加入有限域上的多項式與擴張。
同源結構化資料
本頁與互動版共用同一個物件與既有語言 edition;未新增證明或人工審定。
原始 MKO JSON · 純文字 Markdown