one_mulVec

Mathlib.Data.Matrix.Mul

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

English

Left multiplying a column vector by the identity matrix leaves the vector unchanged.

Русский

Левое умножение вектора на единичную матрицу оставляет вектор без изменений.

LaTeX

$$1 ·ᵥ v = v$$

Lean4

@[simp]
theorem one_mulVec (v : m → α) : 1 *ᵥ v = v := by
  ext
  rw [← diagonal_one, mulVec_diagonal, one_mul]

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

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

Разделы

Аффилиация

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