MachineChecked

Lean repository linked

Three proofs of the Benedetto-Fickus theorem

Dustin G. Mixon, Tom Needham, Clayton Shonkwiler, Soledad Villar · 2021

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.

Report this listing