Theorem nndist_toAdd
Modification history
2025-02-26 19:52
Mathlib/Topology/MetricSpace/Defs.lean
chore (Topology/MetricSpace): remove duplicate instances (#22304) …
Modified nndist_toAddView on Github →2024-11-23 00:05
Mathlib/Topology/MetricSpace/Defs.lean
chore(Algebra/Group/TypeTags): Remove porting notes related to lean4#1910, use new notation everywhere (#19369) …
Modified nndist_toAddView on Github →