noncomputable instance instStarAlgebraPiQComplex {n : Type u_1} [Fintype n] : starAlgebra (PiQ fun (x : n) => ℂ)

Equations

• instStarAlgebraPiQComplex = piStarAlgebra

noncomputable instance instQuantumSetPiQComplex {n : Type u_1} [Fintype n] : QuantumSet (PiQ fun (x : n) => ℂ)

Equations

• instQuantumSetPiQComplex = Pi.quantumSet

theorem EuclideanSpace.comul_eq {n : Type u_1} [Fintype n] [DecidableEq n] (x : PiQ fun (x : n) => ℂ) : let e := fun (i j : n) => if i = j then 1 else 0; CoalgebraStruct.comul x = ∑ i : n, x i • e i ⊗ₜ[ℂ] e i

theorem SimpleGraph.toQuantumGraph {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : QuantumGraph (EuclideanSpace ℂ V) (Matrix.toEuclideanLin (adjMatrix ℂ G))

a finite simple graph is a quantum graph

theorem quantumGraph_numOfEdges_of_classical {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : QuantumGraph.NumOfEdges (Matrix.toEuclideanLin (SimpleGraph.adjMatrix ℂ G)) = ∑ i : V, ∑ j : V, SimpleGraph.adjMatrix ℂ G i j

theorem SimpleGraph.conjTranspose_adjMatrix {V : Type u_1} {α : Type u_2} (G : SimpleGraph V) [DecidableRel G.Adj] [NonAssocSemiring α] [StarRing α] : (adjMatrix α G).conjTranspose = adjMatrix α G

theorem SimpleGraph.adjMatrix_toEuclideanLin_isReal {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : LinearMap.IsReal (Matrix.toEuclideanLin (adjMatrix ℂ G))

theorem SimpleGraph.adjMatrix_toEuclideanLin_symmMap {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : (symmMap ℂ (EuclideanSpace ℂ V) (EuclideanSpace ℂ V)) (Matrix.toEuclideanLin (adjMatrix ℂ G)) = Matrix.toEuclideanLin (adjMatrix ℂ G)

theorem SimpleGraph.adjMatrix_irreflexive {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : Matrix.toEuclideanLin (adjMatrix ℂ G) •ₛ 1 = 0