Def Cauchy.prod

Modification history

2019-07-09 20:34

src/topology/uniform_space/completion.lean

refactor(topology/*): define and use dense_inducing (#1193) …

Deleted Cauchy.prod View on Github →

2018-10-15 13:33

analysis/topology/completion.lean

feat(analysis/topology): group completion

Added Cauchy.prod View on Github →