star_eq_conjTranspose — Mathlib

English

For any square matrix M with entries in a star-typed algebra, the star operation equals the conjugate transpose: star M = M^H.

Русский

Для любой квадратной матрицы с элементами в алгебре со звездой операция звезды равна сопряжённому транспонированию: star M = M^H.

LaTeX

$$$ \text{star } M = M^H $$$

Lean4

theorem star_eq_conjTranspose [Star α] (M : Matrix m m α) : star M = Mᴴ :=
  rfl

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