# 方程式

方程式要求兩個表達式在指定變數範圍內取相等值；解是使等式成立的允許值。

mko-equation · definition · v0.10.0



## 數學敘述

給定兩個具有共同語境的表達式 L(x)、R(x)，方程式 L(x)=R(x) 的解集由所有使兩側皆有定義且值相等的允許 x 組成。





## 代表公式（精確 TeX）

x+1=3





## 成立條件


- 變數的允許範圍、表達式型別與運算規則已明示。





## 符號作用域


- x — 待求或驗證的變數
- = — 兩側值相等的條件





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

方程式不是單一表達式；等號左右各有一個表達式，並且必須在共同的變數範圍中解讀。

驗證候選解時，需把值代入原方程式並分別計算兩側。兩側都定義且相等，該值才屬於解集。

對兩側加減相同量，或乘以相同量，可把原等式的解帶到新等式；若要保持完全相同的解集，乘數必須非零。除以同一量時也必須先證明該量非零；一次方程規則不能自動外推到所有方程。

常見誤解是只化簡一側、乘零後仍宣稱解集不變、除以可能為零的式子、把表達式當方程式，或求得候選值後不代回原式檢查。





## 已採用的推導導讀

[方程式：在定義域內解 x²/(x−1)=1/(x−1)](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-equation-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [變數與代數式](https://ocme.evemisslab.com/zh-Hant/mko/mko-variable-expression/) — 方程式以兩個有共同語境的表達式構成。





## 驗證界線

整數係數的一元線性方程可做精確有限重算，但不構成所有方程求解算法的完備性或正確性證明。

not_formalized

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





## 下一個義務

建立帶明示論域的等式、解集與等價變形聲明，分離非零除數等前提。





## 同源結構化資料

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

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