Commit 2025-08-04 10:34 00fb2584

View on Github →

chore(AbstractCompletion): universe polymorphism (#27762)

Estimated changes

Modified Mathlib/Topology/UniformSpace/AbstractCompletion.lean

modified theorem AbstractCompletion.compare_comp_eq_compare

added structure AbstractCompletion.{v,

deleted structure AbstractCompletion