finrank_fin_fun — Mathlib

English

If an R-vector space M has dimension n, then M is linearly isomorphic to the function space Fin n → R.

Русский

Если размерность векторного пространства M над R равна n, то M взаимно однородно линейно с пространством Fin n → R.

LaTeX

$$$ (\\operatorname{Module.rank} R M = n) \\Rightarrow \\exists e: M \\simeq_R \\mathrm{Fin}\\,n \\to R. $$$

Lean4

/-- The vector space of functions on `Fin n` has `finrank` equal to `n`. -/
theorem finrank_fin_fun {n : ℕ} : finrank R (Fin n → R) = n := by simp

Похожие утверждения