Graph Seidel matrix over a ring

import Mathlib

set_option autoImplicit false

namespace Conway99Formal.FiniteFields

open Matrix SimpleGraph

variable {V : Type*} [Fintype V] [DecidableEq V]

/-- The all-ones matrix on the actual vertex carrier. -/
def J (R : Type*) [One R] : Matrix V V R := Matrix.of fun _ _ => 1















/-- The Seidel matrix in the same vertex coordinates as the adjacency operator. -/
def seidel (G : SimpleGraph V) [DecidableRel G.Adj] (R : Type*)
    [Ring R] [DecidableEq R] : Matrix V V R := J R - 1 - 2 • G.adjMatrix R












end Conway99Formal.FiniteFields