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
feat: Finite order elements have norm one (#9516) This lemma already existed, but with an impractical spelling. From LeanAPAP