フィールド（体）上方にて、スクウェアマトリックス（正方行列）はインバース（逆）を持つ、もしも、そのデターミナント（行列式）が非ゼロである場合、そしてその場合に限って、そして、インバース（逆）はこれであることの記述/証明
話題
About: マトリックス（行列）たちスペース（空間）
この記事の目次
開始コンテキスト
- 読者は、リング（環）上方のスクウェアマトリックス（正方行列）のデターミナント（行列式）の定義を知っている。
- 読者は、リング（環）上方のスクウェアマトリックス（正方行列）のインバース（逆）の定義を知っている。
- 読者は、任意のコミュータティブ（可換）リング（環）上方にて、任意のスクウェアマトリックス（正方行列）たちのプロダクト（積）のデターミナント（行列式）は当該マトリックス（行列）たちのデターミナント（行列式）たちのプロダクト（積）であるという命題を認めている。
- 読者は、任意のコミュータティブ（可換）リング（環）上方の任意のスクウェアマトリックス（正方行列）のデターミナント（行列式）のラプラス展開およびその系を認めている。
ターゲットコンテキスト
- 読者は、任意のフィールド（体）上方にて、任意のスクウェアマトリックス（正方行列）はインバース（逆）を持つ、もしも、そのデターミナント（行列式）が非ゼロである場合、そしてその場合に限って、そして、インバース（逆）はこれであるという命題の記述および証明を得る。
オリエンテーション
本サイトにてこれまで議論された定義たちの一覧があります。
本サイトにてこれまで議論された命題たちの一覧があります。
本体
1: 構造化された記述
ここに'構造化された記述'のルールたちがある。
エンティティ（実体）たち:
\(F\): \(\in \{\text{ 全てのフィールド（体）たち }\}\)
\(n\): \(\in \mathbb{N} \setminus \{0\}\)
\(M\): \(\in \{\text{ 全ての } n \times n R \text{ マトリックス（行列）たち }\}\)
//
ステートメント（言明）たち:
(
\(det M \neq 0\)
\(\iff\)
\(\exists M^{-1}\)
)
\(\land\)
(
\(\exists M^{-1}\)
\(\implies\)
\({M^{-1}}^j_l = 1 / det M M_{l, j}\)
)
//
2: 証明
全体戦略: ステップ1: \(M^{-1}\)は存在すると仮定して、\(det M \neq 0\)であることを見る; ステップ2: \(det M \neq 0\)であると仮定して、\(M^{-1}\)は存在することを見る、\({M^{-1}}^j_l = 1 / det M M_{l, j}\)であることを見ることによって。
ステップ1:
\(M^{-1}\)が存在すると仮定しよう。
\(M M^{-1} = I\)。
\(det (M M^{-1}) = det I = 1\)、しかし、\(det (M M^{-1}) = det M det M^{-1}\)、任意のコミュータティブ（可換）リング（環）上方にて、任意のスクウェアマトリックス（正方行列）たちのプロダクト（積）のデターミナント（行列式）は当該マトリックス（行列）たちのデターミナント（行列式）たちのプロダクト（積）であるという命題によって。
したがって、\(det M \neq 0\)。
ステップ2:
\(det M \neq 0\)であると仮定しよう。
任意のコミュータティブ（可換）リング（環）上方の任意のスクウェアマトリックス（正方行列）のデターミナント（行列式）のラプラス展開およびその系によって、\(det M \delta^j_{j'} = \sum_{l \in \{1, ..., m\}} M^j_l M_{j', l}\)および\(det M \delta^l_{l'} = \sum_{j \in \{1, ..., m\}} M^j_l M_{j, l'}\)。
それが意味するのは、\({M^{-1}}^j_l = 1 / det M M_{l, j}\)、したがって、\(M^{-1}\)は存在する。
