階乘

數學敘述

函數 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 倍，或用超出安全整數範圍的浮點值冒充精確結果。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 自然數 — 階乘的輸入與輸出均為自然數。
• 四則運算 — 後繼遞迴與有限乘積使用自然數乘法。

驗證界線

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

not_formalized

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

下一個義務

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

同源結構化資料

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