star_mulVec

Mathlib.LinearAlgebra.Matrix.ConjTranspose

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

← MathLib Explorer

English

(single i j a)ᴴ = single j i (star a).

Русский

(единичный элемент)ᴴ = единичный элемент наоборот со звездой

LaTeX

$$(\\text{single } i j a)^{\\mathsf{H}} = \\text{single } j i (\\star a)$$

Lean4

theorem star_mulVec [Fintype n] [StarRing α] (M : Matrix m n α) (v : n → α) : star (M *ᵥ v) = star v ᵥ* Mᴴ :=
  funext fun _ => (star_dotProduct_star _ _).symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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