Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-30 10:41 e67f2adf

View on Github →

chore(analysis/topology/uniform_space): remove redundant prod_uniformity (redundant to uniformity_prod)

Estimated changes

deleted theorem prod_uniformity
modified theorem uniformity_prod