Conjugate of a matrix

This file defines the conjugate of a matrix, matrix.conj with the notation ᴴᵀ (i.e., xᴴᵀ i j = star (x i j)), and shows basic properties about it.

def Matrix.conj {α : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [Star α] (x : Matrix n₁ n₂ α) : Matrix n₁ n₂ α

conjugate of matrix defined as $\bar{x} := {(x^*)}^\top$, i.e., $\bar{x}_{ij}=\overline{x_{ij}}$

Equations

• x.conj = x.conjTranspose.transpose

def Matrix.«term_ᴴᵀ» : Lean.TrailingParserDescr

Postfix notation ᴴᵀ for Matrix.conj.

Equations

• Matrix.«term_ᴴᵀ» = Lean.ParserDescr.trailingNode `Matrix.«term_ᴴᵀ» 1024 1024 (Lean.ParserDescr.symbol "ᴴᵀ")

theorem Matrix.conj_apply {α : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [Star α] (x : Matrix n₁ n₂ α) (i : n₁) (j : n₂) : x.conj i j = star (x i j)

theorem Matrix.conj_conj {α : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [InvolutiveStar α] (x : Matrix n₁ n₂ α) : x.conj.conj = x

theorem Matrix.conj_add {α : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [AddMonoid α] [StarAddMonoid α] (x y : Matrix n₁ n₂ α) : (x + y).conj = x.conj + y.conj

theorem Matrix.conj_smul {α : Type u_2} {n₁ : Type u_3} {n₂ : Type u_4} {R : Type u_1} [Star R] [Star α] [SMul R α] [StarModule R α] (c : R) (x : Matrix n₁ n₂ α) : (c • x).conj = star c • x.conj

theorem Matrix.conj_conjTranspose {α : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [InvolutiveStar α] (x : Matrix n₁ n₂ α) : x.conj.conjTranspose = x.transpose

theorem Matrix.conjTranspose_conj {α : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [InvolutiveStar α] (x : Matrix n₁ n₂ α) : x.conjTranspose.conj = x.transpose

theorem Matrix.transpose_conj_eq_conjTranspose {α : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [Star α] (x : Matrix n₁ n₂ α) : x.conj.transpose = x.conjTranspose

theorem Matrix.IsHermitian.conj {α : Type u_1} {n : Type u_2} [Star α] {x : Matrix n n α} (hx : x.IsHermitian) : x.conj = x.transpose

theorem Matrix.conj_mul {α : Type u_1} {m : Type u_2} {n : Type u_3} {p : Type u_4} [Fintype n] [CommSemiring α] [StarRing α] (x : Matrix m n α) (y : Matrix n p α) : (x * y).conj = x.conj * y.conj

theorem Matrix.conj_one {α : Type u_1} {n : Type u_2} [DecidableEq n] [Semiring α] [StarRing α] : conj 1 = 1

theorem Matrix.conj_zero {α : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [AddMonoid α] [StarAddMonoid α] : conj 0 = 0