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 _ _