四則運算

數學敘述

四則運算以兩個輸入形成結果；運算是否有定義、結果是否仍在原數系中，必須連同數系與除零等邊界一起指定。

代表公式（精確 TeX）

a+b

成立條件

• a 與 b 屬於已指定的數系。
• 使用減法與除法時，必須另行檢查結果範圍與除數不為零等條件。

符號作用域

• a — 左運算元
• b — 右運算元
• + — 加法運算

直觀、定義與常見誤解

加法合併數量，乘法可描述等量群組的重複合併；減法尋找差，除法尋找等分或比值。每個運算都必須在明確數系中解讀。

自然數對加法與乘法封閉，但例如 3−5 不再是自然數，3÷2 也不是自然數整除結果。擴張到整數、有理數或實數會改變哪些結果可用。

本條目的 a+b 是加法代表式，不是四種運算的完整公式列舉；乘法 AST 與各數系的精確代數規則留待後續版本。

常見誤解是認為四則運算在所有數系都無條件封閉，或把除以零當作普通除法結果。

已採用的推導導讀

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

前置知識

• 自然數 — 以自然數提供基本數量與後繼算術的第一個運算語境。

驗證界線

本條目是運算家族的概念候選；尚未對四種運算及各數系邊界建立完整計算或形式 Evidence。

not_formalized

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

下一個義務

分別指定自然數與擴張數系中的加減乘除、封閉條件及除零邊界，再建立精確 Lean 聲明。

同源結構化資料

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