rank_fin_fun

Mathlib.LinearAlgebra.Dimension.Constructions

URI: https://scilib.ai/kg/mathlib#rank_fin_fun

English

For the finite set Fin n, the dimension of (Fin n → R) over R is n.

Русский

Для множества Fin n размерность пространства (Fin n → R) над R равна n.

LaTeX

$$$ \\operatorname{Module.rank} R (\\mathrm{Fin}\\,n \\to R) = n. $$$

Lean4

theorem rank_fin_fun (n : ℕ) : Module.rank R (Fin n → R) = n := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru