star_apply — Mathlib

English

Let M be an n×n matrix over a type equipped with a star operation. Then the (i,j) entry of the adjoint equals the star of the (j,i) entry of M, i.e. (M*)_{ij} = (M_{ji})*.

Русский

Пусть M — матрица размером n×n над типом, на котором задано сопряжённое преобразование. Тогда элемент (i, j) сопряжённого транспонирования равен сопряжённому элементу (j, i) матрицы M: (M*)_{ij} = (M_{ji})*.

LaTeX

$$$(M^{*})_{ij} = (M_{ji})^{*}$$$

Lean4

@[simp]
theorem star_apply [Star α] (M : Matrix n n α) (i j) : (star M) i j = star (M j i) :=
  rfl

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