Hermitian matrices have a Jordan algebra structure given by A * B := 2⁻¹ • (A.toMat * B.toMat + B.toMat * A.toMat). We call this operation HermitianMat.symmMul, but it's available as * multiplication scoped under HermMul. When A and B commute, this reduces to standard matrix multiplication.

def HermitianMat.symmMul {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A B : HermitianMat d 𝕜) : HermitianMat d 𝕜

Equations

• A.symmMul B = ⟨2⁻¹ • (↑A * ↑B + ↑B * ↑A), ⋯⟩

theorem HermitianMat.symmMul_comm {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A B : HermitianMat d 𝕜) : A.symmMul B = B.symmMul A

@[simp]

theorem HermitianMat.symmMul_zero {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A : HermitianMat d 𝕜) : A.symmMul 0 = 0

@[simp]

theorem HermitianMat.zero_symmMul {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A : HermitianMat d 𝕜) : symmMul 0 A = 0

theorem HermitianMat.symmMul_toMat {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A B : HermitianMat d 𝕜) : ↑(A.symmMul B) = 2⁻¹ • (↑A * ↑B + ↑B * ↑A)

@[simp]

theorem HermitianMat.symmMul_of_commute {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] {A B : HermitianMat d 𝕜} [Invertible 2] (hAB : Commute ↑A ↑B) : ↑(A.symmMul B) = ↑A * ↑B

theorem HermitianMat.symmMul_self {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A : HermitianMat d 𝕜) [Invertible 2] : ↑(A.symmMul A) = ↑A * ↑A

@[simp]

theorem HermitianMat.symmMul_one {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A : HermitianMat d 𝕜) [Invertible 2] [DecidableEq d] : A.symmMul 1 = A

@[simp]

theorem HermitianMat.one_symmMul {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A : HermitianMat d 𝕜) [Invertible 2] [DecidableEq d] : symmMul 1 A = A

@[simp]

theorem HermitianMat.symmMul_neg_one {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A : HermitianMat d 𝕜) [Invertible 2] [DecidableEq d] : A.symmMul (-1) = -A

@[simp]

theorem HermitianMat.neg_one_symmMul {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A : HermitianMat d 𝕜) [Invertible 2] [DecidableEq d] : (-1).symmMul A = -A

def HermMul.instCommMagmaHermitianMat {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] : CommMagma (HermitianMat d 𝕜)

Equations

• HermMul.instCommMagmaHermitianMat = { mul := HermitianMat.symmMul, mul_comm := ⋯ }

theorem HermMul.mul_eq_symmMul {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] (A B : HermitianMat d 𝕜) : A * B = A.symmMul B

theorem HermMul.instIsCommJordanHermitianMat {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] : IsCommJordan (HermitianMat d 𝕜)

def HermMul.instMulZeroClassHermitianMat {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] : MulZeroClass (HermitianMat d 𝕜)

Equations

• HermMul.instMulZeroClassHermitianMat = { toMul := HermMul.instCommMagmaHermitianMat.toMul, toZero := SubtractionMonoid.toSubNegZeroMonoid.toNegZeroClass.toZero, zero_mul := ⋯, mul_zero := ⋯ }

def HermMul.instMulZeroOneClassHermitianMat {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] [DecidableEq d] [Invertible 2] : MulZeroOneClass (HermitianMat d 𝕜)

Equations

• One or more equations did not get rendered due to their size.

def HermMul.instNonUnitalNonAssocRingHermitianMat {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] : NonUnitalNonAssocRing (HermitianMat d 𝕜)

Equations

• One or more equations did not get rendered due to their size.

def HermMul.instNonAssocRingHermitianMat {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [Field 𝕜] [StarRing 𝕜] [Invertible 2] [DecidableEq d] : NonAssocRing (HermitianMat d 𝕜)

Equations

• One or more equations did not get rendered due to their size.

theorem HermMul.instIsScalarTowerRealHermitianMat {d : Type u_1} {𝕜 : Type u_2} [Fintype d] [RCLike 𝕜] : IsScalarTower ℝ (HermitianMat d 𝕜) (HermitianMat d 𝕜)