Your Sendov and Phelps–Rodriguez formalization has been added to LeanPool, with source attribution and Apache-2.0 licensing preserved. Merged import: https://github.com/Vilin97/lean-pool/pull/556 Thank you for making the formalization available.
Activity