star_mul — Mathlib

English

The conjugate transpose reverses the order of multiplication: (MN)^* = N^* M^* for matrices M,N over a star-ring.

Русский

Сопряжённое транспонирование обращает порядок произведения: (MN)^* = N^* M^* для матриц M и N над кольцом со звёздочкой.

LaTeX

$$$(MN)^{*} = N^{*} M^{*}$$$

Lean4

/-- A version of `star_mul` for `*` instead of `*`. -/
theorem star_mul [Fintype n] [NonUnitalNonAssocSemiring α] [StarRing α] (M N : Matrix n n α) :
    star (M * N) = star N * star M :=
  conjTranspose_mul _ _

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