まとめ

Mathlib の線形代数では，ベクトル空間を Module K V として読みます． 線形写像 V →ₗ[K] W，部分空間 Submodule K V，行列 Matrix m n R は，いずれも数学的な構造とその公理を bundled structure として持ちます．

証明を書くときは，まず #check で補題の型を確認し，simp，module，rw，ext，linear_combination などを必要に応じて使います．

形式化の tips

線形代数の形式化では，紙の証明で省略している「どの空間の元か」を Lean に明示する必要があります．

1. 体 K とベクトル空間 V を分ける．
2. ベクトル空間は [AddCommGroup V] [Module K V] として仮定する．
3. 線形写像は関数ではなく V →ₗ[K] W として扱う．
4. 部分空間は Submodule K V であり，集合として使うときは coercion が働く．
5. span の証明では，生成元が span に入ることと，和・スカラー倍で閉じることを使う．