# 階乘

自然數 n 的階乘由 0!=1 與後繼遞迴式定義，等於 1 到 n 的正整數乘積。

mko-factorial · definition · v0.10.0



## 數學敘述

函數 F:N→N 由 F(0)=1 與 F(n+1)=(n+1)F(n) 唯一遞迴決定；慣用記號為 n!。





## 代表公式（精確 TeX）

F(n)





## 成立條件


- n 是自然數，且自然數包含 0。





## 符號作用域


- F — 階乘函數的代表記號
- n — 自然數輸入
- ! — 階乘慣用後綴記號





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

0! 定義為 1。對自然數 n，(n+1)!=(n+1)·n!；因此 n>0 時，n!=1·2·…·n。

階乘成長很快，精確計算應使用任意精度整數，不應以浮點近似冒充精確值。

階乘會出現在排列計數中，但『n! 計數 n 元集合的排列』是另需證明的定理，不是遞迴定義本身。

常見誤解是把 0! 當成 0、把 n! 當成 n 倍，或用超出安全整數範圍的浮點值冒充精確結果。





## 已採用的推導導讀

[階乘：遞迴定義的唯一性、乘積形式與 5! 的計算](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-factorial-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [自然數](https://ocme.evemisslab.com/zh-Hant/mko/mko-natural-number/) — 階乘的輸入與輸出均為自然數。
- [四則運算](https://ocme.evemisslab.com/zh-Hant/mko/mko-arithmetic-operations/) — 後繼遞迴與有限乘積使用自然數乘法。





## 驗證界線

BigInt 可重算有限自然數的階乘值與遞迴見證，但不構成排列計數、整除性或漸近定理的證明。

not_formalized

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





## 下一個義務

綁定 Nat.factorial、factorial_zero、factorial_succ 與本 MKO 的自然數慣例。





## 同源結構化資料

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

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