norm_replicateCol

Mathlib.Analysis.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.norm_replicateCol

English

The (ordinary) norm of replicateCol ι v equals the norm of v: ∥replicateCol ι v∥ = ∥v∥.

Русский

Норма матрицы replicateCol ι v равна норме v: ∥replicateCol ι v∥ = ∥v∥.

LaTeX

$$$\|\mathrm{replicateCol}_{\iota} v\| = \|v\|.$$$

Lean4

@[simp]
theorem norm_replicateCol (v : m → α) : ‖replicateCol ι v‖ = ‖v‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_replicateCol v

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

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

Разделы

Аффилиация

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