norm_single

Mathlib.Analysis.InnerProductSpace.PiL2

URI: https://scilib.ai/kg/mathlib#EuclideanSpace.norm_single

English

For Finite n, finrank of EuclideanSpace 𝕜 (Fin n) equals n.

Русский

Для Fin n размерность EuclideanSpace 𝕜 (Fin n) равна n.

LaTeX

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

Lean4

@[simp]
theorem norm_single (i : ι) (a : 𝕜) : ‖EuclideanSpace.single i (a : 𝕜)‖ = ‖a‖ :=
  PiLp.norm_toLp_single 2 (fun _ => 𝕜) i a

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

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

Разделы

Аффилиация

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