Theorem: pointDual_comm (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p q : { p // p ≠ 0 }
⊢ ↑p ∈ ↑(pointDual q) ↔ ↑q ∈ ↑(pointDual p)
Tactic:
rw [mem_pointDual, mem_pointDual, real_inner_comm]
State after:
no goals