Commit 2024-10-02 17:17 5cb57a1a
View on Github →feat: golf proof of Fréchet–von Neumann–Jordan theorem (#17349)
Exploit algebraic automation, including the new module
tactic, more heavily in the proof of the Fréchet–von Neumann–Jordan theorem (i.e., the theorem that a norm satisfying the parallellogram identity comes from an inner product).