Mathematics in Lean 日本語訳

• 1. イントロダクション
  • 1.1. 本書の始め方
  • 1.2. 概要
• 2. 基礎
  • 2.1. 計算
  • 2.2. 代数的構造における等式の証明
  • 2.3. 定理と補題を使う
  • 2.4. applyとrwをさらに活用する
  • 2.5. 代数構造についての事実の証明
• 3. 論理
  • 3.1. 含意と全称記号
  • 3.2. 存在量化子
  • 3.3. 否定
  • 3.4. 連言と必要十分条件
  • 3.5. 選言
  • 3.6. 数列と収束
• 4. 集合と関数
  • 4.1. 集合
  • 4.2. 関数
  • 4.3. シュレーダー＝ベルンシュタインの定理
• 5. 初等整数論
  • 5.1. 無理根
  • 5.2. 帰納法と再帰
  • 5.3. 無限に存在する素数
• 6. 構造体
  • 6.1. 構造体の定義
  • 6.2. 代数構造
  • 6.3. ガウス整数の構築
• 7. 階層構造
  • 7.1. 基礎
  • 7.2. 射
  • 7.3. 部分対象
• 8. 群と環
  • 8.1. モノイドと群
  • 8.2. 環
• 9. 線形代数
  • 9.1. ベクトル空間と線形写像
  • 9.2. 部分空間と商空間
  • 9.3. 自己準同型
  • 9.4. 行列・基底・次元
• 10. 位相
  • 10.1. フィルタ
  • 10.2. 距離空間
  • 10.3. 位相空間
• 11. 微分
  • 11.1. 初等的な微分法
  • 11.2. ノルム空間の微分法
• 12. 積分と測度論
  • 12.1. 初等的な積分
  • 12.2. 測度論
  • 12.3. 積分

この翻訳について

この翻訳は有志による 非公式 翻訳です．翻訳に際して分かりやすさのために表現を大きく変えた箇所があります．また，用語の訳が一般的でない・誤りを含む可能性があります．必要に応じて原文 Mathematics in Lean ( GitHub )をご覧ください．

原文にはライセンスが無かったため，原著者より許諾をいただいて翻訳させていただいています．（ Zulip chat ）

誤字脱字・内容の誤りの指摘・フォークからのPull Request・フォークによる翻訳の改変等歓迎いたします．ご指摘は 当該リポジトリ にてIssue・Pull Requestで受け付けております．

翻訳に際して，機械翻訳サービス DeepL翻訳 を参考にしました．

バージョン情報

この翻訳は原文のcommit e3d23850cb3cea5016f98d5ca25160b9a74727b9 に基づいています．