Skip to content
Journals Garden

$\mathbf{F}^n$ and coordinates (LADR 1.11)

  • $\mathbf{F}^n$ and coordinates (LADR 1.11) #Card
    • $\mathbf{F}^n$ の定義と「第 $k$ 座標」とは？

Back

Section titled “Back”

$\mathbf{F}^n$ は $\mathbf{F}$ の要素からなる長さ $n$ のリスト全体： $$\mathbf{F}^n={(x_1,\dots,x_n):x_k\in\mathbf{F},\ k=1,\dots,n}.$$ $(x_1,\dots,x_n)\in\mathbf{F}^n$ と $k\in{1,\dots,n}$ について、$x_k$ を第 $k$ 座標と呼ぶ。 $\mathbf{F}=\mathbf{R}$、$n=2,3$ なら従来の $\mathbf{R}^2,\mathbf{R}^3$ に一致。

Lean

Section titled “Lean”

Mathlib では Fin n → F（または EuclideanSpace F (Fin n) で内積つき）。座標は関数適用 x k。