Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.nndist_eq'

Modification history

2021-08-24 09:54
src/topology/metric_space/basic.lean
feat(data/real/nnreal): upgrade `nnabs` to a `monoid_with_zero_hom` (#8844) …
Added real.nndist_eq'View on Github →