← Mathematical handbook

def Verification.constantOneMatrix (α : Type u_1) : Matrix α α ℝ

Equations

• Verification.constantOneMatrix α = Matrix.of fun (x x_1 : α) => 1

theorem Verification.constant_trace_identity {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (A : Matrix α α ℝ) (B : Matrix β β ℝ) (D : Matrix α β ℝ) (hA : A + A.transpose = 2 • constantOneMatrix α) (hB : B + B.transpose = 2 • constantOneMatrix β) (hD : ∑ i : α, ∑ j : β, D i j = 1) : (A * D * B * D.transpose).trace + (A * D * B.transpose * D.transpose).trace = 2

The checkerboard trace identity uses all-ones symmetric parts and total mass one.