mul_apply

Mathlib.LinearAlgebra.UnitaryGroup

URI: https://scilib.ai/kg/mathlib#Matrix.UnitaryGroup.mul_apply

English

The linear map associated to the product AB equals the composition of the linear maps toLin'(A) and toLin'(B).

Русский

Линейное отображение, связанное с AB, равно композиции toLin'(A) и toLin'(B).

LaTeX

$$toLin'(A B) = (toLin' A) ∘ (toLin' B) for A,B ∈ unitaryGroup n α.$$

Lean4

@[simp]
theorem mul_apply : ⇑(A * B) = A.1 * B.1 :=
  rfl

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

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

Разделы

Аффилиация

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