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

Estimated changes