`BookProof.FriedrichsSquare.opGraph_frExt` (A : D →ₗ[ℂ] F) (hdense : Dense (D : Set F)) (hsym : SymmetricOn D A) : opGraph (frExt A hdense hsym) = factorRel A

Initializing...

`BookProof.FriedrichsSquare.opGraph_frExt` (A : D →ₗ[ℂ] F) (hdense : Dense (D : Set F)) (hsym : SymmetricOn D A) : opGraph (frExt A hdense hsym) = factorRel A · Prove2Me