Commit 2024-01-09 09:25 6520136b

View on Github →

feat: Finite order elements have norm one (#9516) This lemma already existed, but with an impractical spelling. From LeanAPAP

Estimated changes