Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-07 22:43 bf224080

View on Github →

chore(topology/algebra/group_completion): missing namespace (#1518)

Estimated changes

Modified src/topology/algebra/group_completion.lean

deleted theorem coe_zero

added theorem uniform_space.completion.coe_zero