Commit 2024-06-10 11:56 ec8ad89d

View on Github →

chore: move ProperSpace instances to ProperSpace.lean (#13659) This means MetricSpace.Basic no longer needs to depend on MetricSpace.ProperSpace.

Estimated changes