Lean repository linked
Three proofs of the Benedetto-Fickus theorem
arXiv:2112.02916 · arXiv
Lean formalisations (1)
JD-Jones-ASES/finite-quantum-designs-lean at 5938504ecc63
Linked by the repository’s formalization.yaml.
Project review: self-assessed
Audit: awaiting publication.