# 有限含一環

有限含一環在同一完整有限載體上具加法阿貝爾群、乘法結合律、左右分配律及與零不同的乘法單位元。

mko-finite-unital-ring · definition · v0.10.0



## 數學敘述

在同一有限載體X上給完整加法表與乘法表。加法須為阿貝爾群；乘法須結合；乘法對加法左右分配；並存在唯一乘法單位元1且1不等於加法單位元0。本輪不要求乘法交換。





## 代表公式（精確 TeX）

R(X)





## 成立條件


- 載體標籤為0到n-1，兩個n乘n運算表皆完整。
- 資格由全部元素對或三元組精確核對；有限抽樣不替代環公理。





## 符號作用域


- R — 有限含一環紀錄
- X — 共同有限載體
- 0 — 加法單位元
- 1 — 乘法單位元





## 直觀、定義與常見誤解

先由加法表找0與加法逆元，再核乘法結合與左右分配。

乘法單位元必須雙側作用且與0不同。

交換環、整環、域、理想與商環另立節點，不由本資格自動推出。

把只有乘法單位元的有限表、只通過幾個分配樣本的結構，或乘法交換性當作含一環的全部定義。





## 已採用的推導導讀

[有限含一環：證明模 4 的加法表與乘法表構成含一環](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-finite-unital-ring-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [有限阿貝爾群](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-abelian-group/) — 環的加法結構須在同一加法表上成為阿貝爾群。
- [四則運算](https://ocme.evemisslab.com/zh-Hant/mko/mko-arithmetic-operations/) — 加法與乘法是共同載體上的二元運算。
- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 兩個完整表表示X乘X到X的總函數。





## 驗證界線

只分類所給完整有限雙表；不外推任意環，也不宣稱交換、無零因子或每個非零元可逆。

not_formalized

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





## 下一個義務

加入有限交換環、雙邊理想與商環。





## 同源結構化資料

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

[原始 MKO JSON](https://ocme.evemisslab.com/data/mko/finite-unital-ring.json) · [純文字 Markdown](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-unital-ring/index.md)