conjTranspose_single — Mathlib

English

(single i j a)ᴴ = single j i (star a).

Русский

(одиночный элемент)ᴴ = элемент наоборот со звездой

LaTeX

$$(\\text{single } i j a)^{\\mathsf{H}} = \\text{single } j i (\\star a)$$

Lean4

@[simp]
theorem conjTranspose_single [DecidableEq n] [DecidableEq m] [AddMonoid α] [StarAddMonoid α] (i : m) (j : n) (a : α) :
    (single i j a)ᴴ = single j i (star a) :=
  by
  change (single i j a).transpose.map starAddEquiv = single j i (star a)
  simp

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