# 有限雙邊理想

有限環子集若為加法子群且吸收父環的左右乘法，則為雙邊理想。

mko-finite-two-sided-ideal · definition · v0.10.0



## 數學敘述

給有限含一環R與完整子集I。I須非空、對加法及加法逆元封閉，並對所有r屬R、x屬I同時有r乘x與x乘r屬I。資格永遠綁定同一父環。





## 代表公式（精確 TeX）

I(R)





## 成立條件


- 父環以完整雙表通過有限含一環資格，I由互異載體元素完整列出。
- 左右吸收分開量化；有限抽樣不證雙邊性。





## 符號作用域


- I — 雙邊理想
- R — 父環





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

加法子群資格包含0與加法逆元。

左吸收與右吸收各自核全部父環元素。

零理想與整環自身都是雙邊理想；子環或單側理想不能混稱。

只核乘法封閉、只核左吸收，或未綁父環就稱雙邊理想。





## 已採用的推導導讀

[有限雙邊理想：在上三角矩陣環中分開核對左吸收與右吸收](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-finite-two-sided-ideal-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [有限含一環](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-unital-ring/) — 理想運算繼承自同一父環。
- [子集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-subset/) — I是父載體的明示子集。
- [有限阿貝爾群](https://ocme.evemisslab.com/zh-Hant/mko/mko-finite-abelian-group/) — I在加法下須成子群。





## 驗證界線

只核指定完整有限父環與子集；不形成商環，也不宣稱極大／質理想。

not_formalized

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





## 下一個義務

加入有限環的商環與代表元良定性。





## 同源結構化資料

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

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