instStar — Mathlib

English

If α has a star operation, then the square matrices Matrix n n α carry a star operation defined by conjugate transpose: star M = M^H.

Русский

Если у α есть операция звезды, то квадратные матрицы Matrix n n α получают операцию star, определяемую сопряжённым транспонированием: star M = M^H.

LaTeX

$$$ \text{instance } [Star α] : Star (Matrix n n α) \text{ where } star := conjTranspose $$$

Lean4

/-- When `α` has a star operation, square matrices `Matrix n n α` have a star
operation equal to `Matrix.conjTranspose`. -/
instance [Star α] : Star (Matrix n n α) where star := conjTranspose

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