Conjugate of a matrix #
This file defines the conjugate of a matrix, matrix.conj with the notation of this being ᴴᵀ (i.e., xᴴᵀ i j = star (x i j)), and shows basic properties about it.
theorem
matrix.conj_apply
{α : Type u_1}
{n₁ : Type u_2}
{n₂ : Type u_3}
[has_star α]
(x : matrix n₁ n₂ α)
(i : n₁)
(j : n₂) :
x.conj i j = has_star.star (x i j)
theorem
matrix.conj_conj
{α : Type u_1}
{n₁ : Type u_2}
{n₂ : Type u_3}
[has_involutive_star α]
(x : matrix n₁ n₂ α) :
theorem
matrix.conj_add
{α : Type u_1}
{n₁ : Type u_2}
{n₂ : Type u_3}
[add_monoid α]
[star_add_monoid α]
(x y : matrix n₁ n₂ α) :
theorem
matrix.conj_conj_transpose
{α : Type u_1}
{n₁ : Type u_2}
{n₂ : Type u_3}
[has_involutive_star α]
(x : matrix n₁ n₂ α) :
x.conj.conj_transpose = x.transpose
theorem
matrix.conj_transpose_conj
{α : Type u_1}
{n₁ : Type u_2}
{n₂ : Type u_3}
[has_involutive_star α]
(x : matrix n₁ n₂ α) :
x.conj_transpose.conj = x.transpose
theorem
matrix.is_hermitian.conj
{α : Type u_1}
{n : Type u_2}
[has_star α]
{x : matrix n n α}
(hx : x.is_hermitian) :
theorem
matrix.conj_one
{α : Type u_1}
{n : Type u_2}
[decidable_eq n]
[comm_semiring α]
[star_ring α] :