Chapter 02: 線形代数

Mathlib における基本的な線形代数を扱います．

参考: * Mathematics in Lean, 10. Linear Algebra: https://leanprover-community.github.io/mathematics_in_lean/C10_Linear_Algebra.html * Math in Lean: linear algebra: https://leanprover-community.github.io/theories/linear_algebra.html

主に次の対象が中心になります．

• Module R M: 加法群や加法モノイドの上のスカラー倍構造
• V →ₗ[K] W: 線形写像
• Submodule K V: 部分空間・部分加群
• LinearIndependent，Basis，finrank
• Matrix m n R: 行列

Mathlib では，ベクトル空間は専用の VectorSpace 型クラスではなく，体 K 上の Module K V として扱います． これは半環上の半加群や環上の加群まで同じ枠組みで扱うためです．

import Mathlib

namespace PracticeChapter02

open scoped BigOperators
open scoped Matrix