star_vec

Mathlib.LinearAlgebra.Matrix.Vec

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

English

The star operation commutes with vectorization: star(vec A) = vec(A.map star).

Русский

Звёздная операция применима к векторизации: star(vec A) = vec(A.map star).

LaTeX

$$$$\operatorname{star}(\operatorname{vec}(A)) = (A)_{\text{map}}^{\ast}\,\operatorname{vec}$$$$

Lean4

theorem star_vec [Star R] (x : Matrix m n R) : star x.vec = (x.map star).vec :=
  rfl

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

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

Разделы

Аффилиация

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