`BookProof.FriedrichsSquare.mem_flipGraph_iff` {A : D →ₗ[ℂ] F} {p : WithLp 2 (F × F)} : p ∈ flipGraph A ↔ ((WithLp.ofLp p).2, -(WithLp.ofLp p).1) ∈ clGraph A

Initializing...

`BookProof.FriedrichsSquare.mem_flipGraph_iff` {A : D →ₗ[ℂ] F} {p : WithLp 2 (F × F)} : p ∈ flipGraph A ↔ ((WithLp.ofLp p).2, -(WithLp.ofLp p).1) ∈ clGraph A · Prove2Me