Commit 2024-10-02 17:17 5cb57a1a

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).