det_conjTranspose — Mathlib

English

Let R be a ring with an involution and M a square matrix over R. Then det(M^H) equals the involution of det M.

Русский

Пусть R — кольцо с инволюцией, M — квадратная матрица над R. Тогда det(M^H) = det(M)^H.

LaTeX

$$$\\\\det(M^{\\\\ast}) = (\\\\det M)^{\\\\ast}$$$

Lean4

@[simp]
theorem det_conjTranspose [StarRing R] (M : Matrix m m R) : det Mᴴ = star (det M) :=
  ((starRingEnd R).map_det _).symm.trans <| congr_arg star M.det_transpose

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