conjTranspose_smul_self

Mathlib.LinearAlgebra.Matrix.ConjTranspose

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

← MathLib Explorer

English

Corollary of ConjTranspose Smul: (c • M)^H = star c • M^H.

Русский

Следствие: (c • M)^H = star c • M^H.

LaTeX

$$$ (c \cdot M)^{H} = \overline{c} \cdot M^{H} $$$

Lean4

theorem conjTranspose_smul_self [Mul α] [StarMul α] (c : α) (M : Matrix m n α) :
    (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ :=
  conjTranspose_smul_non_comm c M star_mul

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

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

Разделы

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

Аффилиация

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