Theorem: pointDual.α (src/Polar.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
p : { p // p ≠ 0 }
⊢ (pointDual p).α = ‖↑p‖⁻¹
Tactic:
rfl
State after:
no goals