Mathlib.Data.Matrix.ConjTranspose

Matrix.conjTranspose definition

[Star α] (M : Matrix m n α) : Matrix n m α

Full source

/-- The conjugate transpose of a matrix defined in term of `star`. -/
def conjTranspose [Star α] (M : Matrix m n α) : Matrix n m α :=
  M.transpose.map star

Matrix conjugate transpose

Informal description

Given a matrix $M$ of size $m \times n$ with entries in a type $\alpha$ equipped with a star operation, the conjugate transpose of $M$, denoted $M^H$, is the $n \times m$ matrix obtained by taking the transpose of $M$ and applying the star operation to each entry.

Matrix.term_ᴴ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped postfix:1024 "ᴴ" => Matrix.conjTranspose

Conjugate transpose of a matrix

Informal description

The notation `ᴴ` is defined as a postfix operator for the conjugate transpose of a matrix. Given a matrix $M$ with entries in a star ring (a ring equipped with a star operation), $Mᴴ$ denotes its conjugate transpose, which is the matrix obtained by taking the transpose of $M$ and applying the star operation to each entry.

Matrix.conjTranspose_stdBasisMatrix theorem

 [DecidableEq n] [DecidableEq m] [AddMonoid α] [StarAddMonoid α] (i : m) (j : n) (a : α) :
  (stdBasisMatrix i j a)ᴴ = stdBasisMatrix j i (star a)

Full source

@[simp]
lemma conjTranspose_stdBasisMatrix [DecidableEq n] [DecidableEq m] [AddMonoid α]
    [StarAddMonoid α] (i : m) (j : n) (a : α) :
    (stdBasisMatrix i j a)ᴴ = stdBasisMatrix j i (star a) := by
  show (stdBasisMatrix i j a).transpose.map starAddEquiv = stdBasisMatrix j i (star a)
  simp

Conjugate Transpose of Standard Basis Matrix: $(\text{stdBasisMatrix}(i,j,a))^H = \text{stdBasisMatrix}(j,i,\overline{a})$

Informal description

Let $m$ and $n$ be types with decidable equality, $\alpha$ be an additive monoid with a star operation that is an additive monoid homomorphism. For any indices $i \in m$, $j \in n$ and element $a \in \alpha$, the conjugate transpose of the standard basis matrix $\text{stdBasisMatrix}(i,j,a)$ satisfies: \[ (\text{stdBasisMatrix}(i,j,a))^H = \text{stdBasisMatrix}(j,i,\overline{a}) \] where $\overline{a}$ denotes the star of $a$.

Matrix.diagonal_conjTranspose theorem

[AddMonoid α] [StarAddMonoid α] (v : n → α) : (diagonal v)ᴴ = diagonal (star v)

Full source

@[simp]
theorem diagonal_conjTranspose [AddMonoid α] [StarAddMonoid α] (v : n → α) :
    (diagonal v)ᴴ = diagonal (star v) := by
  rw [conjTranspose, diagonal_transpose, diagonal_map (star_zero _)]
  rfl

Conjugate Transpose of Diagonal Matrix Equals Diagonal of Starred Vector

Informal description

Let $\alpha$ be an additive monoid equipped with a star operation that is an additive monoid homomorphism. For any vector $v : n \to \alpha$, the conjugate transpose of the diagonal matrix constructed from $v$ is equal to the diagonal matrix constructed from the star of $v$, i.e., $$(\text{diag}(v))^H = \text{diag}(\overline{v}).$$

Matrix.diag_conjTranspose theorem

[Star α] (A : Matrix n n α) : diag Aᴴ = star (diag A)

Full source

@[simp]
theorem diag_conjTranspose [Star α] (A : Matrix n n α) :
    diag Aᴴ = star (diag A) :=
  rfl

Diagonal of Conjugate Transpose: $\text{diag}(A^H) = \overline{\text{diag}(A)}$

Informal description

For any square matrix $A$ of size $n \times n$ with entries in a type $\alpha$ equipped with a star operation, the diagonal of the conjugate transpose $A^H$ is equal to the star of the diagonal of $A$, i.e., \[ \text{diag}(A^H) = \overline{\text{diag}(A)}. \]

Matrix.star_dotProduct_star theorem

: star v ⬝ᵥ star w = star (w ⬝ᵥ v)

Full source

theorem star_dotProduct_star : starstar v ⬝ᵥ star w = star (w ⬝ᵥ v) := by simp [dotProduct]

Star Dot Product Identity: $\overline{v} \cdot \overline{w} = \overline{w \cdot v}$

Informal description

For any vectors $v$ and $w$ in a star ring, the dot product of the star of $v$ and the star of $w$ equals the star of the dot product of $w$ and $v$, i.e., $\overline{v} \cdot \overline{w} = \overline{w \cdot v}$.

Matrix.star_dotProduct theorem

: star v ⬝ᵥ w = star (star w ⬝ᵥ v)

Full source

theorem star_dotProduct : starstar v ⬝ᵥ w = star (starstar w ⬝ᵥ v) := by simp [dotProduct]

Star Dot Product Identity: $\overline{v} \cdot w = \overline{\overline{w} \cdot v}$

Informal description

For any vectors $v$ and $w$ in a star ring, the dot product of the conjugate of $v$ with $w$ equals the conjugate of the dot product of the conjugate of $w$ with $v$, i.e., \[ \overline{v} \cdot w = \overline{\overline{w} \cdot v}. \]

Matrix.dotProduct_star theorem

: v ⬝ᵥ star w = star (w ⬝ᵥ star v)

Full source

theorem dotProduct_star : v ⬝ᵥ star w = star (w ⬝ᵥ star v) := by simp [dotProduct]

Dot Product Conjugate Identity: $v \cdot \overline{w} = \overline{w \cdot \overline{v}}$

Informal description

For any vectors $v$ and $w$ with entries in a star ring $\alpha$, the dot product of $v$ with the conjugate transpose of $w$ equals the conjugate of the dot product of $w$ with the conjugate transpose of $v$. In symbols: \[ v \cdot \overline{w} = \overline{w \cdot \overline{v}} \]

Matrix.star_mulVec theorem

[Fintype n] [StarRing α] (M : Matrix m n α) (v : n → α) : star (M *ᵥ v) = star v ᵥ* Mᴴ

Full source

theorem star_mulVec [Fintype n] [StarRing α] (M : Matrix m n α) (v : n → α) :
    star (M *ᵥ v) = starstar v ᵥ* Mᴴ :=
  funext fun _ => (star_dotProduct_star _ _).symm

Star of Matrix-Vector Product Equals Vector-Matrix Product with Conjugate Transpose

Informal description

Let $M$ be an $m \times n$ matrix with entries in a star ring $\alpha$, and let $v$ be an $n$-dimensional vector with entries in $\alpha$. Then the star of the matrix-vector product $M \cdot v$ equals the vector-matrix product of the star of $v$ with the conjugate transpose of $M$, i.e., \[ \overline{M \cdot v} = \overline{v} \cdot M^H. \]

Matrix.star_vecMul theorem

[Fintype m] [StarRing α] (M : Matrix m n α) (v : m → α) : star (v ᵥ* M) = Mᴴ *ᵥ star v

Full source

theorem star_vecMul [Fintype m] [StarRing α] (M : Matrix m n α) (v : m → α) :
    star (v ᵥ* M) = MᴴMᴴ *ᵥ star v :=
  funext fun _ => (star_dotProduct_star _ _).symm

Star of Vector-Matrix Product Equals Conjugate Transpose Matrix Applied to Star of Vector

Informal description

Let $M$ be an $m \times n$ matrix with entries in a star ring $\alpha$, and let $v$ be a vector of length $m$ with entries in $\alpha$. Then the star of the vector-matrix product $v \cdot M$ equals the matrix-vector product of the conjugate transpose $M^H$ with the star of $v$, i.e., \[ \overline{v \cdot M} = M^H \cdot \overline{v}. \]

Matrix.mulVec_conjTranspose theorem

[Fintype m] [StarRing α] (A : Matrix m n α) (x : m → α) : Aᴴ *ᵥ x = star (star x ᵥ* A)

Full source

theorem mulVec_conjTranspose [Fintype m] [StarRing α] (A : Matrix m n α) (x : m → α) :
    AᴴAᴴ *ᵥ x = star (starstar x ᵥ* A) :=
  funext fun _ => star_dotProduct _ _

Conjugate Transpose Matrix-Vector Product Identity: $A^H \cdot x = \overline{\overline{x} \cdot A}$

Informal description

Let $A$ be an $m \times n$ matrix over a star ring $\alpha$ with finitely many rows, and let $x$ be a vector in $\alpha^m$. Then the matrix-vector product of the conjugate transpose $A^H$ with $x$ equals the conjugate of the vector-matrix product of the conjugate of $x$ with $A$, i.e., \[ A^H \cdot x = \overline{\overline{x} \cdot A}. \]

Matrix.vecMul_conjTranspose theorem

[Fintype n] [StarRing α] (A : Matrix m n α) (x : n → α) : x ᵥ* Aᴴ = star (A *ᵥ star x)

Full source

theorem vecMul_conjTranspose [Fintype n] [StarRing α] (A : Matrix m n α) (x : n → α) :
    x ᵥ* Aᴴ = star (A *ᵥ star x) :=
  funext fun _ => dotProduct_star _ _

Vector-Matrix Product with Conjugate Transpose: $x \cdot A^H = \overline{A \cdot \overline{x}}$

Informal description

Let $\alpha$ be a star ring, $A$ be an $m \times n$ matrix with entries in $\alpha$, and $x$ be a vector in $\alpha^n$. Then the vector-matrix product of $x$ with the conjugate transpose of $A$ equals the star of the matrix-vector product of $A$ with the star of $x$. In symbols: \[ x \cdot A^H = \overline{A \cdot \overline{x}} \]

Matrix.conjTranspose_apply theorem

[Star α] (M : Matrix m n α) (i j) : M.conjTranspose j i = star (M i j)

Full source

/-- Tell `simp` what the entries are in a conjugate transposed matrix.

  Compare with `mul_apply`, `diagonal_apply_eq`, etc.
-/
@[simp]
theorem conjTranspose_apply [Star α] (M : Matrix m n α) (i j) :
    M.conjTranspose j i = star (M i j) :=
  rfl

Conjugate Transpose Entry Formula: $(M^H)_{j,i} = \overline{M_{i,j}}$

Informal description

For any matrix $M$ of size $m \times n$ with entries in a type $\alpha$ equipped with a star operation, the $(j, i)$-th entry of the conjugate transpose $M^H$ is equal to the star of the $(i, j)$-th entry of $M$, i.e., $(M^H)_{j,i} = \overline{M_{i,j}}$.

Matrix.conjTranspose_conjTranspose theorem

[InvolutiveStar α] (M : Matrix m n α) : Mᴴᴴ = M

Full source

@[simp]
theorem conjTranspose_conjTranspose [InvolutiveStar α] (M : Matrix m n α) : MᴴMᴴᴴ = M :=
  Matrix.ext <| by simp

Double Conjugate Transpose Identity: $(M^H)^H = M$

Informal description

For any matrix $M$ of size $m \times n$ with entries in a type $\alpha$ equipped with an involutive star operation, the double conjugate transpose of $M$ equals $M$ itself, i.e., $(M^H)^H = M$.

Matrix.conjTranspose_injective theorem

[InvolutiveStar α] : Function.Injective (conjTranspose : Matrix m n α → Matrix n m α)

Full source

theorem conjTranspose_injective [InvolutiveStar α] :
    Function.Injective (conjTranspose : Matrix m n α → Matrix n m α) :=
  (map_injective star_injective).comp transpose_injective

Injectivity of Matrix Conjugate Transpose Operation

Informal description

For any type $\alpha$ with an involutive star operation, the conjugate transpose operation on $m \times n$ matrices with entries in $\alpha$ is injective. That is, if $M^H = N^H$ for matrices $M, N \in \text{Matrix}_{m \times n}(\alpha)$, then $M = N$.

Matrix.conjTranspose_inj theorem

[InvolutiveStar α] {A B : Matrix m n α} : Aᴴ = Bᴴ ↔ A = B

Full source

@[simp] theorem conjTranspose_inj [InvolutiveStar α] {A B : Matrix m n α} : AᴴAᴴ = Bᴴ ↔ A = B :=
  conjTranspose_injective.eq_iff

Conjugate Transpose Equality Criterion: $A^H = B^H \leftrightarrow A = B$

Informal description

For any two $m \times n$ matrices $A$ and $B$ with entries in a type $\alpha$ equipped with an involutive star operation, the conjugate transpose of $A$ equals the conjugate transpose of $B$ if and only if $A = B$. That is, $A^H = B^H \leftrightarrow A = B$.

Matrix.conjTranspose_eq_diagonal theorem

 [DecidableEq n] [AddMonoid α] [StarAddMonoid α] {M : Matrix n n α} {v : n → α} :
  Mᴴ = diagonal v ↔ M = diagonal (star v)

Full source

@[simp]
theorem conjTranspose_eq_diagonal [DecidableEq n] [AddMonoid α] [StarAddMonoid α]
    {M : Matrix n n α} {v : n → α} :
    MᴴMᴴ = diagonal v ↔ M = diagonal (star v) :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
    by rw [diagonal_conjTranspose]

Conjugate Transpose Equals Diagonal Matrix Criterion: $M^H = \text{diag}(v) \leftrightarrow M = \text{diag}(\overline{v})$

Informal description

Let $n$ be a type with decidable equality, and let $\alpha$ be an additive monoid equipped with a star operation that is an additive monoid homomorphism. For any square matrix $M$ of size $n \times n$ with entries in $\alpha$ and any vector $v : n \to \alpha$, the conjugate transpose of $M$ equals the diagonal matrix constructed from $v$ if and only if $M$ itself equals the diagonal matrix constructed from the star of $v$. That is, $$ M^H = \text{diag}(v) \leftrightarrow M = \text{diag}(\overline{v}). $$

Matrix.conjTranspose_zero theorem

[AddMonoid α] [StarAddMonoid α] : (0 : Matrix m n α)ᴴ = 0

Full source

@[simp]
theorem conjTranspose_zero [AddMonoid α] [StarAddMonoid α] : (0 : Matrix m n α)ᴴ = 0 :=
  Matrix.ext <| by simp

Conjugate Transpose of Zero Matrix is Zero Matrix

Informal description

For any type $\alpha$ equipped with an additive monoid structure and a star operation that is compatible with addition, the conjugate transpose of the zero matrix of size $m \times n$ is equal to the zero matrix of size $n \times m$, i.e., $0^H = 0$.

Matrix.conjTranspose_eq_zero theorem

[AddMonoid α] [StarAddMonoid α] {M : Matrix m n α} : Mᴴ = 0 ↔ M = 0

Full source

@[simp]
theorem conjTranspose_eq_zero [AddMonoid α] [StarAddMonoid α] {M : Matrix m n α} :
    MᴴMᴴ = 0 ↔ M = 0 := by
  rw [← conjTranspose_inj (A := M), conjTranspose_zero]

Conjugate Transpose Equals Zero Matrix Criterion: $M^H = 0 \leftrightarrow M = 0$

Informal description

For any $m \times n$ matrix $M$ with entries in a type $\alpha$ equipped with an additive monoid structure and a star operation compatible with addition, the conjugate transpose of $M$ equals the zero matrix if and only if $M$ itself is the zero matrix, i.e., $M^H = 0 \leftrightarrow M = 0$.

Matrix.conjTranspose_one theorem

[DecidableEq n] [NonAssocSemiring α] [StarRing α] : (1 : Matrix n n α)ᴴ = 1

Full source

@[simp]
theorem conjTranspose_one [DecidableEq n] [NonAssocSemiring α] [StarRing α] :
    (1 : Matrix n n α)ᴴ = 1 := by
  simp [conjTranspose]

Conjugate Transpose of Identity Matrix is Identity

Informal description

For any type $n$ with decidable equality and any non-associative semiring $\alpha$ equipped with a star operation satisfying the star ring axioms, the conjugate transpose of the identity matrix in $\text{Matrix}(n, n, \alpha)$ is equal to the identity matrix itself, i.e., $1^H = 1$.

Matrix.conjTranspose_eq_one theorem

[DecidableEq n] [NonAssocSemiring α] [StarRing α] {M : Matrix n n α} : Mᴴ = 1 ↔ M = 1

Full source

@[simp]
theorem conjTranspose_eq_one [DecidableEq n] [NonAssocSemiring α] [StarRing α] {M : Matrix n n α} :
    MᴴMᴴ = 1 ↔ M = 1 :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
    by rw [conjTranspose_one]

Conjugate Transpose Equals Identity Matrix Criterion: $M^H = 1 \leftrightarrow M = 1$

Informal description

For any type $n$ with decidable equality and any non-associative semiring $\alpha$ equipped with a star operation satisfying the star ring axioms, a square matrix $M$ of size $n \times n$ over $\alpha$ has its conjugate transpose equal to the identity matrix if and only if $M$ itself is the identity matrix, i.e., $M^H = 1 \leftrightarrow M = 1$.

Matrix.conjTranspose_natCast theorem

[DecidableEq n] [NonAssocSemiring α] [StarRing α] (d : ℕ) : (d : Matrix n n α)ᴴ = d

Full source

@[simp]
theorem conjTranspose_natCast [DecidableEq n] [NonAssocSemiring α] [StarRing α] (d : ℕ) :
    (d : Matrix n n α)ᴴ = d := by
  simp [conjTranspose, Matrix.map_natCast, diagonal_natCast]

Conjugate Transpose of Diagonal Matrix with Natural Number Entries

Informal description

Let $n$ be a type with decidable equality, $\alpha$ a non-associative semiring equipped with a star operation (forming a star ring), and $d$ a natural number. The conjugate transpose of the diagonal matrix with all diagonal entries equal to $d$ (as an element of $\alpha$) is equal to the matrix itself, i.e., $(dI_n)^H = dI_n$, where $I_n$ denotes the $n \times n$ identity matrix with diagonal entries $d$.

Matrix.conjTranspose_eq_natCast theorem

[DecidableEq n] [NonAssocSemiring α] [StarRing α] {M : Matrix n n α} {d : ℕ} : Mᴴ = d ↔ M = d

Full source

@[simp]
theorem conjTranspose_eq_natCast [DecidableEq n] [NonAssocSemiring α] [StarRing α]
    {M : Matrix n n α} {d : ℕ} :
    MᴴMᴴ = d ↔ M = d :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
    by rw [conjTranspose_natCast]

Equivalence of Conjugate Transpose and Diagonal Matrix with Natural Number Entries: $M^H = dI_n \leftrightarrow M = dI_n$

Informal description

Let $n$ be a type with decidable equality, $\alpha$ a non-associative semiring equipped with a star operation (forming a star ring), $M$ an $n \times n$ matrix over $\alpha$, and $d$ a natural number. The conjugate transpose of $M$ equals the diagonal matrix with all diagonal entries $d$ if and only if $M$ itself equals this diagonal matrix, i.e., $M^H = dI_n \leftrightarrow M = dI_n$, where $I_n$ denotes the $n \times n$ identity matrix with diagonal entries $d$.

Matrix.conjTranspose_ofNat theorem

 [DecidableEq n] [NonAssocSemiring α] [StarRing α] (d : ℕ) [d.AtLeastTwo] : (ofNat(d) : Matrix n n α)ᴴ = OfNat.ofNat d

Full source

@[simp]
theorem conjTranspose_ofNat [DecidableEq n] [NonAssocSemiring α] [StarRing α] (d : ℕ)
    [d.AtLeastTwo] : (ofNat(d) : Matrix n n α)ᴴ = OfNat.ofNat d :=
  conjTranspose_natCast _

Conjugate Transpose of Scalar Matrix with Natural Number ≥ 2 Entries Equals Itself

Informal description

Let $n$ be a type with decidable equality, $\alpha$ a non-associative semiring equipped with a star operation (forming a star ring), and $d \geq 2$ a natural number. The conjugate transpose of the diagonal matrix with all diagonal entries equal to $d$ (interpreted as an element of $\alpha$) is equal to the matrix itself, i.e., $(dI_n)^H = dI_n$, where $I_n$ denotes the $n \times n$ identity matrix with diagonal entries $d$.

Matrix.conjTranspose_eq_ofNat theorem

 [DecidableEq n] [Semiring α] [StarRing α] {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] : Mᴴ = ofNat(d) ↔ M = OfNat.ofNat d

Full source

@[simp]
theorem conjTranspose_eq_ofNat [DecidableEq n] [Semiring α] [StarRing α]
    {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] :
    MᴴMᴴ = ofNat(d) ↔ M = OfNat.ofNat d :=
  conjTranspose_eq_natCast

Characterization of Scalar Matrices via Conjugate Transpose for Natural Numbers ≥ 2: $M^H = dI_n \leftrightarrow M = dI_n$

Informal description

Let $n$ be a type with decidable equality, $\alpha$ a semiring equipped with a star operation (forming a star ring), $M$ an $n \times n$ matrix over $\alpha$, and $d \geq 2$ a natural number. The conjugate transpose of $M$ equals the diagonal matrix with all diagonal entries $d$ if and only if $M$ itself equals this diagonal matrix, i.e., $M^H = dI_n \leftrightarrow M = dI_n$, where $I_n$ denotes the $n \times n$ identity matrix with diagonal entries $d$.

Matrix.conjTranspose_intCast theorem

[DecidableEq n] [Ring α] [StarRing α] (d : ℤ) : (d : Matrix n n α)ᴴ = d

Full source

@[simp]
theorem conjTranspose_intCast [DecidableEq n] [Ring α] [StarRing α] (d : ℤ) :
    (d : Matrix n n α)ᴴ = d := by
  simp [conjTranspose, Matrix.map_intCast, diagonal_intCast]

Conjugate Transpose of Integer Scalar Matrix Equals Itself

Informal description

Let $n$ be a type with decidable equality, $\alpha$ a ring equipped with a star operation (forming a star ring), and $d$ an integer. The conjugate transpose of the scalar matrix $d \cdot I_n$ (where $I_n$ is the $n \times n$ identity matrix) is equal to itself, i.e., $(d \cdot I_n)^H = d \cdot I_n$.

Matrix.conjTranspose_eq_intCast theorem

[DecidableEq n] [Ring α] [StarRing α] {M : Matrix n n α} {d : ℤ} : Mᴴ = d ↔ M = d

Full source

@[simp]
theorem conjTranspose_eq_intCast [DecidableEq n] [Ring α] [StarRing α]
    {M : Matrix n n α} {d : ℤ} :
    MᴴMᴴ = d ↔ M = d :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <|
    by rw [conjTranspose_intCast]

Characterization of Integer Scalar Matrices via Conjugate Transpose: $M^H = d \cdot I_n \leftrightarrow M = d \cdot I_n$

Informal description

Let $n$ be a type with decidable equality, $\alpha$ a ring equipped with a star operation (forming a star ring), and $M$ an $n \times n$ matrix over $\alpha$. For any integer $d$, the conjugate transpose of $M$ equals the scalar matrix $d \cdot I_n$ if and only if $M$ itself equals $d \cdot I_n$, i.e., $M^H = d \cdot I_n \leftrightarrow M = d \cdot I_n$.

Matrix.conjTranspose_add theorem

[AddMonoid α] [StarAddMonoid α] (M N : Matrix m n α) : (M + N)ᴴ = Mᴴ + Nᴴ

Full source

@[simp]
theorem conjTranspose_add [AddMonoid α] [StarAddMonoid α] (M N : Matrix m n α) :
    (M + N)ᴴ = Mᴴ + Nᴴ :=
  Matrix.ext <| by simp

Additivity of Conjugate Transpose for Matrices

Informal description

Let $\alpha$ be a type equipped with an addition operation and a star operation that is compatible with addition. For any two matrices $M$ and $N$ of size $m \times n$ with entries in $\alpha$, the conjugate transpose of their sum equals the sum of their conjugate transposes, i.e., $(M + N)^H = M^H + N^H$.

Matrix.conjTranspose_sub theorem

[AddGroup α] [StarAddMonoid α] (M N : Matrix m n α) : (M - N)ᴴ = Mᴴ - Nᴴ

Full source

@[simp]
theorem conjTranspose_sub [AddGroup α] [StarAddMonoid α] (M N : Matrix m n α) :
    (M - N)ᴴ = Mᴴ - Nᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose of Matrix Difference: $(M - N)^H = M^H - N^H$

Informal description

For any matrices $M$ and $N$ of size $m \times n$ with entries in a type $\alpha$ equipped with an additive group structure and a star operation that is compatible with addition, the conjugate transpose of the difference $M - N$ is equal to the difference of the conjugate transposes $M^H - N^H$.

Matrix.conjTranspose_smul theorem

[Star R] [Star α] [SMul R α] [StarModule R α] (c : R) (M : Matrix m n α) : (c • M)ᴴ = star c • Mᴴ

Full source

/-- Note that `StarModule` is quite a strong requirement; as such we also provide the following
variants which this lemma would not apply to:
* `Matrix.conjTranspose_smul_non_comm`
* `Matrix.conjTranspose_nsmul`
* `Matrix.conjTranspose_zsmul`
* `Matrix.conjTranspose_natCast_smul`
* `Matrix.conjTranspose_intCast_smul`
* `Matrix.conjTranspose_inv_natCast_smul`
* `Matrix.conjTranspose_inv_intCast_smul`
* `Matrix.conjTranspose_ratCast_smul`
-/
@[simp]
theorem conjTranspose_smul [Star R] [Star α] [SMul R α] [StarModule R α] (c : R)
    (M : Matrix m n α) : (c • M)ᴴ = star c • Mᴴ :=
  Matrix.ext fun _ _ => star_smul _ _

Conjugate Transpose of Scalar Multiple: $(c \cdot M)^H = \text{star}(c) \cdot M^H$

Informal description

Let $R$ and $\alpha$ be types equipped with star operations, and let $\alpha$ be a module over $R$ with a compatible star module structure. For any scalar $c \in R$ and any matrix $M \in \text{Matrix}_{m \times n}(\alpha)$, the conjugate transpose of the scalar multiple $c \cdot M$ is equal to the scalar multiple of the conjugate transpose of $M$ with the scalar $\text{star}(c)$, i.e., $$(c \cdot M)^H = \text{star}(c) \cdot M^H.$$

Matrix.conjTranspose_smul_non_comm theorem

 [Star R] [Star α] [SMul R α] [SMul Rᵐᵒᵖ α] (c : R) (M : Matrix m n α)
  (h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a) : (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ

Full source

@[simp]
theorem conjTranspose_smul_non_comm [Star R] [Star α] [SMul R α] [SMul Rᵐᵒᵖ α] (c : R)
    (M : Matrix m n α) (h : ∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a) :
    (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ :=
  Matrix.ext <| by simp [h]

Conjugate transpose of scalar multiplication under non-commutative star condition: $(c \cdot M)^H = \text{op}(\star c) \cdot M^H$

Informal description

Let $R$ and $\alpha$ be types equipped with star operations, and let $\alpha$ have scalar multiplication operations from $R$ and its opposite ring $R^\text{op}$. For any scalar $c \in R$ and matrix $M \in \text{Matrix}_{m \times n}(\alpha)$, if the star operation satisfies $\star(r \cdot a) = \text{op}(\star r) \cdot \star a$ for all $r \in R$ and $a \in \alpha$, then the conjugate transpose of $c \cdot M$ equals $\text{op}(\star c) \cdot M^H$.

Matrix.conjTranspose_smul_self theorem

[Mul α] [StarMul α] (c : α) (M : Matrix m n α) : (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ

Full source

theorem conjTranspose_smul_self [Mul α] [StarMul α] (c : α) (M : Matrix m n α) :
    (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ :=
  conjTranspose_smul_non_comm c M star_mul

Conjugate transpose of scalar multiplication in a star-multiplicative algebra: $(c \cdot M)^H = \text{op}(\star c) \cdot M^H$

Informal description

Let $\alpha$ be a type equipped with a multiplication operation and a star operation that is multiplicative (i.e., $\star(a \cdot b) = \star b \cdot \star a$ for all $a, b \in \alpha$). For any element $c \in \alpha$ and any matrix $M \in \text{Matrix}_{m \times n}(\alpha)$, the conjugate transpose of the scalar multiple $c \cdot M$ is equal to the scalar multiple $\text{op}(\star c) \cdot M^H$, where $M^H$ denotes the conjugate transpose of $M$ and $\text{op}$ denotes the opposite multiplication.

Matrix.conjTranspose_nsmul theorem

[AddMonoid α] [StarAddMonoid α] (c : ℕ) (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ

Full source

@[simp]
theorem conjTranspose_nsmul [AddMonoid α] [StarAddMonoid α] (c : ℕ) (M : Matrix m n α) :
    (c • M)ᴴ = c • Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose Commutes with Natural Number Scalar Multiplication

Informal description

Let $\alpha$ be an additive monoid equipped with a star operation that is an additive monoid homomorphism. For any natural number $c$ and any matrix $M$ of size $m \times n$ with entries in $\alpha$, the conjugate transpose of the scalar multiple $c \cdot M$ is equal to the scalar multiple $c \cdot M^H$, where $M^H$ denotes the conjugate transpose of $M$.

Matrix.conjTranspose_zsmul theorem

[AddGroup α] [StarAddMonoid α] (c : ℤ) (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ

Full source

@[simp]
theorem conjTranspose_zsmul [AddGroup α] [StarAddMonoid α] (c : ℤ) (M : Matrix m n α) :
    (c • M)ᴴ = c • Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose Commutes with Integer Scalar Multiplication

Informal description

Let $\alpha$ be an additive group equipped with a star operation that is compatible with addition. For any integer $c$ and any $m \times n$ matrix $M$ with entries in $\alpha$, the conjugate transpose of the scalar multiple $c \cdot M$ is equal to the scalar multiple $c \cdot M^H$, where $M^H$ denotes the conjugate transpose of $M$.

Matrix.conjTranspose_natCast_smul theorem

 [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) (M : Matrix m n α) :
  ((c : R) • M)ᴴ = (c : R) • Mᴴ

Full source

@[simp]
theorem conjTranspose_natCast_smul [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α]
    (c : ℕ) (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose Commutes with Natural Number Scalar Multiplication: $(c \cdot M)^H = c \cdot M^H$

Informal description

Let $R$ be a semiring, $\alpha$ an additive commutative monoid with a star operation that is an additive monoid homomorphism, and $R$-module structure on $\alpha$. For any natural number $c \in \mathbb{N}$ and any matrix $M \in \text{Matrix}_{m \times n}(\alpha)$, the conjugate transpose of the scalar multiple $(c \cdot M)^H$ is equal to the scalar multiple of the conjugate transpose $c \cdot M^H$, where $M^H$ denotes the conjugate transpose of $M$.

Matrix.conjTranspose_ofNat_smul theorem

 [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) :
  ((ofNat(c) : R) • M)ᴴ = (OfNat.ofNat c : R) • Mᴴ

Full source

@[simp]
theorem conjTranspose_ofNat_smul [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α]
    (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) :
    ((ofNat(c) : R) • M)ᴴ = (OfNat.ofNat c : R) • Mᴴ :=
  conjTranspose_natCast_smul c M

Conjugate Transpose Commutes with Scalar Multiplication by Numerals ≥ 2: $(c \cdot M)^H = c \cdot M^H$

Informal description

Let $R$ be a semiring, $\alpha$ an additive commutative monoid with a star operation that is an additive monoid homomorphism, and $R$-module structure on $\alpha$. For any natural number $c \geq 2$ and any matrix $M \in \text{Matrix}_{m \times n}(\alpha)$, the conjugate transpose of the scalar multiple $(c \cdot M)^H$ is equal to the scalar multiple of the conjugate transpose $c \cdot M^H$, where $M^H$ denotes the conjugate transpose of $M$.

Matrix.conjTranspose_intCast_smul theorem

 [Ring R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ) (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ

Full source

@[simp]
theorem conjTranspose_intCast_smul [Ring R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ)
    (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose Commutes with Integer Scalar Multiplication: $(c \cdot M)^H = c \cdot M^H$

Informal description

Let $R$ be a ring, $\alpha$ an additive commutative group with a star operation that is an additive monoid homomorphism, and $R$-module structure on $\alpha$. For any integer $c \in \mathbb{Z}$ and any matrix $M \in \text{Matrix}_{m \times n}(\alpha)$, the conjugate transpose of the scalar multiple $(c \cdot M)^H$ is equal to the scalar multiple of the conjugate transpose $c \cdot M^H$.

Matrix.conjTranspose_inv_natCast_smul theorem

 [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) (M : Matrix m n α) :
  ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ

Full source

@[simp]
theorem conjTranspose_inv_natCast_smul [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α]
    [Module R α] (c : ℕ) (M : Matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose of Scaled Matrix by Natural Number Inverse: $((c^{-1})M)^H = c^{-1} M^H$

Informal description

Let $R$ be a division semiring and $\alpha$ be an additive commutative monoid equipped with a star operation that is an additive monoid homomorphism, and an $R$-module structure. For any natural number $c \in \mathbb{N}$ and any matrix $M \in \text{Mat}_{m \times n}(\alpha)$, the conjugate transpose of the scaled matrix $(c^{-1} \cdot M)$ is equal to $c^{-1} \cdot M^H$, where $M^H$ denotes the conjugate transpose of $M$.

Matrix.conjTranspose_inv_ofNat_smul theorem

 [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) :
  ((ofNat(c) : R)⁻¹ • M)ᴴ = (OfNat.ofNat c : R)⁻¹ • Mᴴ

Full source

@[simp]
theorem conjTranspose_inv_ofNat_smul [DivisionSemiring R] [AddCommMonoid α] [StarAddMonoid α]
    [Module R α] (c : ℕ) [c.AtLeastTwo] (M : Matrix m n α) :
    ((ofNat(c) : R)⁻¹ • M)ᴴ = (OfNat.ofNat c : R)⁻¹ • Mᴴ :=
  conjTranspose_inv_natCast_smul c M

Conjugate Transpose of Scaled Matrix by Numeric Literal Inverse: $((c^{-1})M)^H = c^{-1} M^H$ for $c \geq 2$

Informal description

Let $R$ be a division semiring and $\alpha$ be an additive commutative monoid equipped with a star operation that is an additive monoid homomorphism, and an $R$-module structure. For any natural number $c \geq 2$ and any matrix $M \in \text{Mat}_{m \times n}(\alpha)$, the conjugate transpose of the scaled matrix $(c^{-1} \cdot M)$ is equal to $c^{-1} \cdot M^H$, where $M^H$ denotes the conjugate transpose of $M$.

Matrix.conjTranspose_inv_intCast_smul theorem

 [DivisionRing R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ) (M : Matrix m n α) :
  ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ

Full source

@[simp]
theorem conjTranspose_inv_intCast_smul [DivisionRing R] [AddCommGroup α] [StarAddMonoid α]
    [Module R α] (c : ℤ) (M : Matrix m n α) : ((c : R)⁻¹ • M)ᴴ = (c : R)⁻¹ • Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose of Scaled Matrix by Integer Inverse: $((c^{-1})M)^H = c^{-1} M^H$

Informal description

Let $R$ be a division ring and $\alpha$ be an additive commutative group equipped with a star operation and an $R$-module structure. For any integer $c \in \mathbb{Z}$ and any matrix $M \in \text{Mat}_{m \times n}(\alpha)$, the conjugate transpose of the scaled matrix $(c^{-1} \cdot M)$ is equal to $c^{-1} \cdot M^H$, where $M^H$ denotes the conjugate transpose of $M$.

Matrix.conjTranspose_ratCast_smul theorem

 [DivisionRing R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℚ) (M : Matrix m n α) :
  ((c : R) • M)ᴴ = (c : R) • Mᴴ

Full source

@[simp]
theorem conjTranspose_ratCast_smul [DivisionRing R] [AddCommGroup α] [StarAddMonoid α] [Module R α]
    (c : ℚ) (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose Commutes with Rational Scalar Multiplication

Informal description

Let $R$ be a division ring and $\alpha$ be an additive commutative group equipped with a star operation and a module structure over $R$. For any rational number $c$ and any matrix $M$ of size $m \times n$ with entries in $\alpha$, the conjugate transpose of the scalar multiple $(c : R) \cdot M$ is equal to the scalar multiple $(c : R)$ of the conjugate transpose of $M$, i.e., $$((c : R) \cdot M)^H = (c : R) \cdot M^H.$$

Matrix.conjTranspose_rat_smul theorem

[AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ) (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ

Full source

theorem conjTranspose_rat_smul [AddCommGroup α] [StarAddMonoid α] [Module ℚ α] (c : ℚ)
    (M : Matrix m n α) : (c • M)ᴴ = c • Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose Commutes with Rational Scalar Multiplication: $(c \cdot M)^H = c \cdot M^H$

Informal description

Let $\alpha$ be an additive commutative group equipped with a star operation and a $\mathbb{Q}$-module structure. For any rational number $c$ and any matrix $M$ of size $m \times n$ with entries in $\alpha$, the conjugate transpose of the scalar multiple $c \cdot M$ is equal to the scalar multiple $c$ of the conjugate transpose of $M$, i.e., $$(c \cdot M)^H = c \cdot M^H.$$

Matrix.conjTranspose_mul theorem

 [Fintype n] [NonUnitalNonAssocSemiring α] [StarRing α] (M : Matrix m n α) (N : Matrix n l α) : (M * N)ᴴ = Nᴴ * Mᴴ

Full source

@[simp]
theorem conjTranspose_mul [Fintype n] [NonUnitalNonAssocSemiring α] [StarRing α] (M : Matrix m n α)
    (N : Matrix n l α) : (M * N)ᴴ = Nᴴ * Mᴴ :=
  Matrix.ext <| by simp [mul_apply]

Conjugate Transpose of Matrix Product: $(MN)^H = N^H M^H$

Informal description

Let $M$ be an $m \times n$ matrix and $N$ be an $n \times l$ matrix with entries in a non-unital non-associative semiring $\alpha$ equipped with a star operation. If $\alpha$ is a star ring and $n$ is a finite type, then the conjugate transpose of the matrix product $MN$ equals the product of the conjugate transposes in reverse order, i.e., $(MN)^H = N^H M^H$.

Matrix.conjTranspose_neg theorem

[AddGroup α] [StarAddMonoid α] (M : Matrix m n α) : (-M)ᴴ = -Mᴴ

Full source

@[simp]
theorem conjTranspose_neg [AddGroup α] [StarAddMonoid α] (M : Matrix m n α) : (-M)ᴴ = -Mᴴ :=
  Matrix.ext <| by simp

Conjugate Transpose of Matrix Negation: $(-M)^H = -M^H$

Informal description

Let $\alpha$ be a type equipped with an additive group structure and a star operation that is compatible with addition. For any matrix $M$ of size $m \times n$ with entries in $\alpha$, the conjugate transpose of the negation of $M$ equals the negation of the conjugate transpose of $M$, i.e., $(-M)^H = -M^H$.

Matrix.conjTranspose_map theorem

 [Star α] [Star β] {A : Matrix m n α} (f : α → β) (hf : Function.Semiconj f star star) : Aᴴ.map f = (A.map f)ᴴ

Full source

theorem conjTranspose_map [Star α] [Star β] {A : Matrix m n α} (f : α → β)
    (hf : Function.Semiconj f star star) : Aᴴ.map f = (A.map f)ᴴ :=
  Matrix.ext fun _ _ => hf _

Conjugate Transpose Commutes with Star-Semiconjugating Map

Informal description

Let $\alpha$ and $\beta$ be types equipped with star operations, and let $A$ be an $m \times n$ matrix with entries in $\alpha$. For any function $f : \alpha \to \beta$ that semiconjugates the star operations (i.e., $f \circ \text{star} = \text{star} \circ f$), the conjugate transpose of the matrix obtained by applying $f$ to each entry of $A$ is equal to applying $f$ to each entry of the conjugate transpose of $A$. In symbols: $$(A^H).\text{map}(f) = (A.\text{map}(f))^H.$$

Matrix.conjTranspose_eq_transpose_of_trivial theorem

[Star α] [TrivialStar α] (A : Matrix m n α) : Aᴴ = Aᵀ

Full source

/-- When `star x = x` on the coefficients (such as the real numbers) `conjTranspose` and `transpose`
are the same operation. -/
@[simp]
theorem conjTranspose_eq_transpose_of_trivial [Star α] [TrivialStar α] (A : Matrix m n α) :
    Aᴴ = Aᵀ := Matrix.ext fun _ _ => star_trivial _

Conjugate Transpose Equals Transpose for Trivial Star Operation

Informal description

For any matrix $A$ of size $m \times n$ with entries in a type $\alpha$ equipped with a star operation that satisfies $\text{star}(x) = x$ for all $x \in \alpha$ (i.e., the star operation is trivial), the conjugate transpose $A^H$ is equal to the transpose $A^\top$.

Matrix.conjTransposeAddEquiv definition

[AddMonoid α] [StarAddMonoid α] : Matrix m n α ≃+ Matrix n m α

Full source

/-- `Matrix.conjTranspose` as an `AddEquiv` -/
@[simps apply]
def conjTransposeAddEquiv [AddMonoid α] [StarAddMonoid α] : MatrixMatrix m n α ≃+ Matrix n m α where
  toFun := conjTranspose
  invFun := conjTranspose
  left_inv := conjTranspose_conjTranspose
  right_inv := conjTranspose_conjTranspose
  map_add' := conjTranspose_add

Additive equivalence of matrix conjugate transpose

Informal description

The function `Matrix.conjTransposeAddEquiv` is an additive equivalence between the space of $m \times n$ matrices and the space of $n \times m$ matrices over a type $\alpha$ equipped with an addition operation and a star operation compatible with addition. It maps a matrix to its conjugate transpose, with the inverse operation also being the conjugate transpose. This equivalence satisfies the property that the conjugate transpose of a sum of matrices is equal to the sum of their conjugate transposes.

Matrix.conjTransposeAddEquiv_symm theorem

[AddMonoid α] [StarAddMonoid α] : (conjTransposeAddEquiv m n α).symm = conjTransposeAddEquiv n m α

Full source

@[simp]
theorem conjTransposeAddEquiv_symm [AddMonoid α] [StarAddMonoid α] :
    (conjTransposeAddEquiv m n α).symm = conjTransposeAddEquiv n m α :=
  rfl

Inverse of Conjugate Transpose Additive Equivalence is Conjugate Transpose

Informal description

For any type $\alpha$ equipped with an addition operation and a star operation compatible with addition, the inverse of the additive equivalence `conjTransposeAddEquiv` between $m \times n$ matrices and $n \times m$ matrices is equal to the additive equivalence `conjTransposeAddEquiv` between $n \times m$ matrices and $m \times n$ matrices. In other words, $(A^H)^H = A$ for any matrix $A$.

Matrix.conjTranspose_list_sum theorem

[AddMonoid α] [StarAddMonoid α] (l : List (Matrix m n α)) : l.sumᴴ = (l.map conjTranspose).sum

Full source

theorem conjTranspose_list_sum [AddMonoid α] [StarAddMonoid α] (l : List (Matrix m n α)) :
    l.sumᴴ = (l.map conjTranspose).sum :=
  map_list_sum (conjTransposeAddEquiv m n α) l

Conjugate Transpose of Matrix List Sum

Informal description

Let $\alpha$ be a type equipped with an addition operation and a star operation compatible with addition. For any list $l$ of $m \times n$ matrices over $\alpha$, the conjugate transpose of the sum of the matrices in $l$ is equal to the sum of the conjugate transposes of the matrices in $l$. That is, $( \sum_{M \in l} M )^H = \sum_{M \in l} M^H$.

Matrix.conjTranspose_multiset_sum theorem

[AddCommMonoid α] [StarAddMonoid α] (s : Multiset (Matrix m n α)) : s.sumᴴ = (s.map conjTranspose).sum

Full source

theorem conjTranspose_multiset_sum [AddCommMonoid α] [StarAddMonoid α]
    (s : Multiset (Matrix m n α)) : s.sumᴴ = (s.map conjTranspose).sum :=
  (conjTransposeAddEquiv m n α).toAddMonoidHom.map_multiset_sum s

Conjugate Transpose of Matrix Multiset Sum

Informal description

Let $\alpha$ be an additive commutative monoid equipped with a star operation compatible with addition. For any multiset $s$ of $m \times n$ matrices over $\alpha$, the conjugate transpose of the sum of the matrices in $s$ is equal to the sum of the conjugate transposes of the matrices in $s$. That is, $(\sum_{M \in s} M)^H = \sum_{M \in s} M^H$.

Matrix.conjTranspose_sum theorem

 [AddCommMonoid α] [StarAddMonoid α] {ι : Type*} (s : Finset ι) (M : ι → Matrix m n α) :
  (∑ i ∈ s, M i)ᴴ = ∑ i ∈ s, (M i)ᴴ

Full source

theorem conjTranspose_sum [AddCommMonoid α] [StarAddMonoid α] {ι : Type*} (s : Finset ι)
    (M : ι → Matrix m n α) : (∑ i ∈ s, M i)ᴴ = ∑ i ∈ s, (M i)ᴴ :=
  map_sum (conjTransposeAddEquiv m n α) _ s

Conjugate Transpose of Finite Sum of Matrices

Informal description

Let $\alpha$ be an additive commutative monoid equipped with a star operation compatible with addition. For any finite set $s$ indexed by type $\iota$ and any family of $m \times n$ matrices $M_i$ over $\alpha$ indexed by $i \in s$, the conjugate transpose of the sum $\sum_{i \in s} M_i$ is equal to the sum of the conjugate transposes $\sum_{i \in s} M_i^H$.

Matrix.conjTransposeLinearEquiv definition

 [CommSemiring R] [StarRing R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] [StarModule R α] :
  Matrix m n α ≃ₗ⋆[R] Matrix n m α

Full source

/-- `Matrix.conjTranspose` as a `LinearMap` -/
@[simps apply]
def conjTransposeLinearEquiv [CommSemiring R] [StarRing R] [AddCommMonoid α] [StarAddMonoid α]
    [Module R α] [StarModule R α] : MatrixMatrix m n α ≃ₗ⋆[R] Matrix n m α :=
  { conjTransposeAddEquiv m n α with map_smul' := conjTranspose_smul }

Star-linear equivalence of matrix conjugate transpose

Informal description

Given a commutative semiring $R$ with a star operation, and an additive commutative monoid $\alpha$ with a star operation compatible with addition and a scalar multiplication by $R$ that respects the star operation, the function `Matrix.conjTransposeLinearEquiv` is a star-linear equivalence between the space of $m \times n$ matrices over $\alpha$ and the space of $n \times m$ matrices over $\alpha$. It maps a matrix to its conjugate transpose and preserves both the linear and star structures.

Matrix.conjTransposeLinearEquiv_symm theorem

 [CommSemiring R] [StarRing R] [AddCommMonoid α] [StarAddMonoid α] [Module R α] [StarModule R α] :
  (conjTransposeLinearEquiv m n R α).symm = conjTransposeLinearEquiv n m R α

Full source

@[simp]
theorem conjTransposeLinearEquiv_symm [CommSemiring R] [StarRing R] [AddCommMonoid α]
    [StarAddMonoid α] [Module R α] [StarModule R α] :
    (conjTransposeLinearEquiv m n R α).symm = conjTransposeLinearEquiv n m R α :=
  rfl

Inverse of Conjugate Transpose Star-Linear Equivalence Equals Transpose Equivalence

Informal description

Given a commutative semiring $R$ with a star operation, and an additive commutative monoid $\alpha$ with a star operation compatible with addition and a scalar multiplication by $R$ that respects the star operation, the inverse of the star-linear equivalence `conjTransposeLinearEquiv` between $m \times n$ matrices and $n \times m$ matrices over $\alpha$ is equal to the star-linear equivalence `conjTransposeLinearEquiv` between $n \times m$ matrices and $m \times n$ matrices over $\alpha$.

Matrix.conjTransposeRingEquiv definition

[Semiring α] [StarRing α] [Fintype m] : Matrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ

Full source

/-- `Matrix.conjTranspose` as a `RingEquiv` to the opposite ring -/
@[simps]
def conjTransposeRingEquiv [Semiring α] [StarRing α] [Fintype m] :
    MatrixMatrix m m α ≃+* (Matrix m m α)ᵐᵒᵖ :=
  { (conjTransposeAddEquiv m m α).trans MulOpposite.opAddEquiv with
    toFun := fun M => MulOpposite.op Mᴴ
    invFun := fun M => M.unopᴴ
    map_mul' := fun M N =>
      (congr_arg MulOpposite.op (conjTranspose_mul M N)).trans (MulOpposite.op_mul _ _) }

Ring equivalence of matrix conjugate transpose with opposite ring multiplication

Informal description

Given a semiring $\alpha$ with a star operation and a finite type $m$, the function `Matrix.conjTransposeRingEquiv` is a ring equivalence between the space of $m \times m$ matrices over $\alpha$ and the opposite ring of such matrices. It maps a matrix $M$ to the conjugate transpose $M^H$ (with the opposite ring multiplication), and its inverse maps an element of the opposite ring back to the conjugate transpose. This equivalence preserves both the additive and multiplicative structures of the rings.

Matrix.conjTranspose_pow theorem

[Semiring α] [StarRing α] [Fintype m] [DecidableEq m] (M : Matrix m m α) (k : ℕ) : (M ^ k)ᴴ = Mᴴ ^ k

Full source

@[simp]
theorem conjTranspose_pow [Semiring α] [StarRing α] [Fintype m] [DecidableEq m] (M : Matrix m m α)
    (k : ℕ) : (M ^ k)ᴴ = Mᴴ ^ k :=
  MulOpposite.op_injective <| map_pow (conjTransposeRingEquiv m α) M k

Conjugate Transpose of Matrix Power: $(M^k)^H = (M^H)^k$

Informal description

Let $\alpha$ be a semiring equipped with a star operation, and let $m$ be a finite type with decidable equality. For any square matrix $M$ of size $m \times m$ over $\alpha$ and any natural number $k$, the conjugate transpose of $M^k$ is equal to the $k$-th power of the conjugate transpose of $M$, i.e., $(M^k)^H = (M^H)^k$.

Matrix.conjTranspose_list_prod theorem

 [Semiring α] [StarRing α] [Fintype m] [DecidableEq m] (l : List (Matrix m m α)) :
  l.prodᴴ = (l.map conjTranspose).reverse.prod

Full source

theorem conjTranspose_list_prod [Semiring α] [StarRing α] [Fintype m] [DecidableEq m]
    (l : List (Matrix m m α)) : l.prodᴴ = (l.map conjTranspose).reverse.prod :=
  (conjTransposeRingEquiv m α).unop_map_list_prod l

Conjugate Transpose of Matrix Product Equals Reverse Product of Conjugate Transposes

Informal description

Let $\alpha$ be a semiring equipped with a star operation, and let $m$ be a finite type with decidable equality. For any list $l$ of $m \times m$ matrices over $\alpha$, the conjugate transpose of the product of the matrices in $l$ is equal to the product of the conjugate transposes of the matrices in $l$ taken in reverse order. That is, $$(l_1 \cdots l_n)^H = l_n^H \cdots l_1^H.$$

Matrix.instStar instance

[Star α] : Star (Matrix n n α)

Full source

/-- When `α` has a star operation, square matrices `Matrix n n α` have a star
operation equal to `Matrix.conjTranspose`. -/
instance [Star α] : Star (Matrix n n α) where star := conjTranspose

Star Operation on Square Matrices via Conjugate Transpose

Informal description

For any type $\alpha$ equipped with a star operation and any natural number $n$, the space of $n \times n$ matrices over $\alpha$ has a star operation defined by the conjugate transpose. That is, for a matrix $M$, the star operation $\star M$ is equal to the conjugate transpose $M^H$.

Matrix.star_eq_conjTranspose theorem

[Star α] (M : Matrix m m α) : star M = Mᴴ

Full source

theorem star_eq_conjTranspose [Star α] (M : Matrix m m α) : star M = Mᴴ :=
  rfl

Star Operation Equals Conjugate Transpose for Square Matrices

Informal description

For any square matrix $M$ of size $m \times m$ with entries in a type $\alpha$ equipped with a star operation, the star operation applied to $M$ is equal to its conjugate transpose, i.e., $M^* = M^H$.

Matrix.star_apply theorem

[Star α] (M : Matrix n n α) (i j) : (star M) i j = star (M j i)

Full source

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

Star Operation on Matrix Entries: $(M^*)_{ij} = (M_{ji})^*$

Informal description

For any type $\alpha$ equipped with a star operation and any natural number $n$, the star operation applied to an $n \times n$ matrix $M$ over $\alpha$ satisfies $(M^*)_{ij} = (M_{ji})^*$ for all indices $i,j$, where $M^*$ denotes the star of $M$ and $(M_{ji})^*$ denotes the star of the matrix entry $M_{ji}$.

Matrix.instInvolutiveStar instance

[InvolutiveStar α] : InvolutiveStar (Matrix n n α)

Full source

instance [InvolutiveStar α] : InvolutiveStar (Matrix n n α) where
  star_involutive := conjTranspose_conjTranspose

Involutive Star Operation on Square Matrices

Informal description

For any type $\alpha$ equipped with an involutive star operation and any natural number $n$, the space of $n \times n$ matrices over $\alpha$ inherits an involutive star operation. This means that for any matrix $M$, the double star operation satisfies $\star(\star M) = M$.

Matrix.instStarAddMonoid instance

[AddMonoid α] [StarAddMonoid α] : StarAddMonoid (Matrix n n α)

Full source

/-- When `α` is a `*`-additive monoid, `Matrix.star` is also a `*`-additive monoid. -/
instance [AddMonoid α] [StarAddMonoid α] : StarAddMonoid (Matrix n n α) where
  star_add := conjTranspose_add

Star Additive Monoid Structure on Square Matrices

Informal description

For any type $\alpha$ equipped with an addition operation and a star operation that is compatible with addition, the space of $n \times n$ matrices over $\alpha$ inherits a star additive monoid structure. This means that the star operation distributes over matrix addition, i.e., $\star(M + N) = \star M + \star N$ for any matrices $M$ and $N$ of the same size.

Matrix.instStarModule instance

[Star α] [Star β] [SMul α β] [StarModule α β] : StarModule α (Matrix n n β)

Full source

instance [Star α] [Star β] [SMul α β] [StarModule α β] : StarModule α (Matrix n n β) where
  star_smul := conjTranspose_smul

Star Module Structure on Square Matrices

Informal description

For any types $\alpha$ and $\beta$ equipped with star operations, where $\beta$ is a module over $\alpha$ with a compatible star module structure, the space of $n \times n$ matrices over $\beta$ inherits a star module structure from $\beta$. This means that for any scalar $c \in \alpha$ and matrix $M \in \text{Matrix}_{n \times n}(\beta)$, the star operation satisfies $\star(c \cdot M) = \star c \cdot \star M$.

Matrix.instStarRing instance

[Fintype n] [NonUnitalSemiring α] [StarRing α] : StarRing (Matrix n n α)

Full source

/-- When `α` is a `*`-(semi)ring, `Matrix.star` is also a `*`-(semi)ring. -/
instance [Fintype n] [NonUnitalSemiring α] [StarRing α] : StarRing (Matrix n n α) where
  star_add := conjTranspose_add
  star_mul := conjTranspose_mul

Star Ring Structure on Square Matrices

Informal description

For any finite type $n$ and any non-unital semiring $\alpha$ equipped with a star ring structure, the space of $n \times n$ matrices over $\alpha$ inherits a star ring structure. This means that the star operation is compatible with matrix addition and multiplication, satisfying $\star(M + N) = \star M + \star N$ and $\star(M * N) = \star N * \star M$ for any matrices $M$ and $N$.

Matrix.star_mul theorem

[Fintype n] [NonUnitalNonAssocSemiring α] [StarRing α] (M N : Matrix n n α) : star (M * N) = star N * star M

Full source

/-- A version of `star_mul` for `*` instead of `*`. -/
theorem star_mul [Fintype n] [NonUnitalNonAssocSemiring α] [StarRing α] (M N : Matrix n n α) :
    star (M * N) = star N * star M :=
  conjTranspose_mul _ _

Star Operation on Matrix Product: $\star(MN) = \star N \star M$

Informal description

For any $n \times n$ matrices $M$ and $N$ with entries in a non-unital non-associative semiring $\alpha$ equipped with a star operation, if $\alpha$ is a star ring and $n$ is finite, then the star operation applied to the matrix product $M * N$ equals the product of the star operations applied to $N$ and $M$ in reverse order, i.e., $\star(M * N) = \star N * \star M$.

Matrix.conjTranspose_submatrix theorem

 [Star α] (A : Matrix m n α) (r_reindex : l → m) (c_reindex : o → n) :
  (A.submatrix r_reindex c_reindex)ᴴ = Aᴴ.submatrix c_reindex r_reindex

Full source

@[simp]
theorem conjTranspose_submatrix [Star α] (A : Matrix m n α) (r_reindex : l → m)
    (c_reindex : o → n) : (A.submatrix r_reindex c_reindex)ᴴ = Aᴴ.submatrix c_reindex r_reindex :=
  ext fun _ _ => rfl

Conjugate Transpose of Submatrix Equals Reindexed Submatrix of Conjugate Transpose

Informal description

Let $A$ be an $m \times n$ matrix with entries in a type $\alpha$ equipped with a star operation. For any reindexing functions $r_{\text{reindex}} : l \to m$ and $c_{\text{reindex}} : o \to n$, the conjugate transpose of the submatrix $A_{\text{submatrix}}(r_{\text{reindex}}, c_{\text{reindex}})$ is equal to the submatrix of the conjugate transpose $A^H$ with rows and columns reindexed by $c_{\text{reindex}}$ and $r_{\text{reindex}}$ respectively. That is, $$(A_{\text{submatrix}}(r_{\text{reindex}}, c_{\text{reindex}}))^H = A^H_{\text{submatrix}}(c_{\text{reindex}}, r_{\text{reindex}}).$$

Matrix.conjTranspose_reindex theorem

[Star α] (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) : (reindex eₘ eₙ M)ᴴ = reindex eₙ eₘ Mᴴ

Full source

theorem conjTranspose_reindex [Star α] (eₘ : m ≃ l) (eₙ : n ≃ o) (M : Matrix m n α) :
    (reindex eₘ eₙ M)ᴴ = reindex eₙ eₘ Mᴴ :=
  rfl

Conjugate Transpose Commutes with Matrix Reindexing: $(\text{reindex}(e_m, e_n)(M))^H = \text{reindex}(e_n, e_m)(M^H)$

Informal description

Let $\alpha$ be a type equipped with a star operation, and let $M$ be an $m \times n$ matrix with entries in $\alpha$. For any bijections $e_m : m \leftrightarrow l$ and $e_n : n \leftrightarrow o$, the conjugate transpose of the reindexed matrix $\text{reindex}(e_m, e_n)(M)$ is equal to the reindexed conjugate transpose $\text{reindex}(e_n, e_m)(M^H)$. In other words, $$(\text{reindex}(e_m, e_n)(M))^H = \text{reindex}(e_n, e_m)(M^H).$$

Notation