Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dist_prod_same_left

Modification history

2022-04-12 05:57
src/topology/metric_space/basic.lean
feat(topology/metric_space/basic): some lemmas about dist (#13343) …
Added dist_prod_same_leftView on Github →