finrank_euclideanSpace — Mathlib

English

For a natural number n, finrank 𝕜 (EuclideanSpace 𝕜 (Fin n)) equals n.

Русский

Для натурального числа n размерность пространства Евклидова пространства над 𝕜 по модулю Fin n равна n.

LaTeX

$$$\operatorname{finrank}_{𝕜}(\mathrm{EuclideanSpace}\; 𝕜\; (\mathrm{Fin}\ n)) = n$$$

Lean4

@[simp]
theorem finrank_euclideanSpace : Module.finrank 𝕜 (EuclideanSpace 𝕜 ι) = Fintype.card ι := by simp [WithLp]

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