norm_replicateRow

Mathlib.Analysis.Matrix

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

English

ReplicateRow preserves the norm: ∥replicateRow ι v∥ = ∥v∥.

Русский

Реплицирование ряда сохраняет норму: ∥replicateRow ι v∥ = ∥v∥.

LaTeX

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

Lean4

@[simp]
theorem norm_replicateRow (v : n → α) : ‖replicateRow ι v‖ = ‖v‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_replicateRow v

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

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

Разделы

Аффилиация

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