This project has been added to [Lean Pool](https://github.com/Vilin97/lean-pool), which maintains completed Lean formalizations against its pinned Lean and Mathlib versions. Merged import: [#458](https://github.com/Vilin97/lean-pool/pull/458), [#467](https://github.com/Vilin97/lean-pool/pull/467). Original attribution and licensing are retained.
Activity