# 有限群

有限群由有限集合與完整封閉Cayley表構成，並滿足結合律、唯一單位元及每元素逆元。

mko-finite-group · definition · v0.10.0



## 數學敘述

有限集合G配備二元運算*。若運算對G封閉、對所有三元組結合、存在雙側單位元且每元素有雙側逆元，則(G,*)為有限群。完整Cayley表可窮舉核對指定有限模型。





## 代表公式（精確 TeX）

G(S)





## 成立條件


- 元素以0到n-1標記，題目提供n×n完整運算表。
- 抽樣列或少數三元組不證群；結合律必須窮舉全部n³三元組。





## 符號作用域


- G — 有限群候選
- S — 有限載體





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

封閉表示表內每格輸出仍是G元素。

結合律比較(a*b)*c與a*(b*c)的全部三元組，不等同交換律。

單位元需左右都成立；逆元也需左右乘都得到同一單位元。

只看表的對稱性或幾個案例就宣稱是群，或把單側單位／逆元當雙側。





## 已採用的推導導讀

[有限群：以完整 Cayley 表核對群公理](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-finite-group-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [集合](https://ocme.evemisslab.com/zh-Hant/mko/mko-set/) — 群有固定載體集合。
- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 二元運算必須總且單值。
- [二元關係與集合投影](https://ocme.evemisslab.com/zh-Hant/mko/mko-relation/) — Cayley表以輸入對指定輸出。
- [數學證明](https://ocme.evemisslab.com/zh-Hant/mko/mko-proof/) — 群資格需封閉全部公理責任。





## 驗證界線

完整有限表可精確核對指定候選；不外推無限群或未列運算。

not_formalized

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





## 下一個義務

加入子群、同態、陪集、正規子群與商群。





## 同源結構化資料

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

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