completion) : add injective_coe (#10454)

Commit

4 years ago

feat(topology/uniform_space/completion) : add injective_coe (#10454) Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>

Author

mariainesdff

Parents

cbe1d379

mathlib3 3dfa3496 - feat(topology/uniform_space/completion) : add injective_coe (#10454)

mathlib3
3dfa3496 - feat(topology/uniform_space/completion) : add injective_coe (#10454)