# 矩陣表示的實平面線性映射

先在 R²→R² 的矩陣切片驗證加法與純量相容，不把帶非零平移的仿射式叫線性映射。

mko-linear-transformation · definition · v0.10.0



## 數學敘述

映射 T:R²→R² 為線性映射，當且僅當對所有向量 u、v 與實純量 c，T(u+v)=T(u)+T(v)、T(cv)=cT(v)。本輪 T(v)=Mv，M 是2×2實矩陣，向量以列向量約定。仿射式 F(v)=Mv+b 在全實平面上為線性映射，當且僅當 b 是零向量。





## 代表公式（精確 TeX）

T(v)





## 成立條件


- 明示全實平面的定義域、陪域、列向量與2×2矩陣，不泛化成任意維度或任意映射的有限抽樣判定。
- 題庫矩陣、向量及純量採安全整數，以精確運算求值。
- 零矩陣與零向量合法；線性式不等於必須可逆，也不要求斜率或行列式非零。





## 符號作用域


- T — 矩陣表示的實平面線性映射
- v — 兩分量實列向量





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

Mv 的每個分量是該行與 v 的對應乘積和，不是逐項乘後仍輸出矩陣。加法相容與純量相容是所有合法輸入的條件，不由少數測點替任意函數背書。

矩陣表示給出一個明示的線性模型；本輪題目計算等式兩側的實際值，不將這些有限計算另包裝成普遍 proof。

若 b≠0，F(0)=b≠0，已不能線性；若 b=0 則回到 Mv。仿射判定不靠改無關的 M 元素湊變種；可逆、單射與等距另有條件。

把圖上直線或仿射式的非零截距當成線性，或由有限測點判定任意函數線性。





## 已採用的推導導讀

[線性映射：證明 v↦Mv 線性，且仿射式 Mv+b 線性當且僅當 b=0](https://ocme.evemisslab.com/zh-Hant/derivations/derivation-mko-linear-transformation-01/)原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。





## 前置知識


- [有限矩陣的尺寸、索引與轉置](https://ocme.evemisslab.com/zh-Hant/mko/mko-matrix/) — 固定2×2矩陣與索引。
- [固定基底下的平面向量](https://ocme.evemisslab.com/zh-Hant/mko/mko-vector/) — 兩分量向量的加法及純量運算。
- [函數映射](https://ocme.evemisslab.com/zh-Hant/mko/mko-function-mapping/) — 總函數的輸入與輸出宣告。





## 驗證界線

2×2整數切片可精確核對；全實數線性性與矩陣／LinearMap 橋未新增形式 Evidence。

not_formalized

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





## 下一個義務

橋接 Matrix.mulVecLin 與標準基底的 R² 加法、純量相容；不是微分線性化工作。





## 同源結構化資料

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

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