feat: add instances of MetricSpace, NormedAddGroup, and NormedAddCommGroup for DirectLimit#39673
Open
drocta wants to merge 36 commits into
Open
feat: add instances of MetricSpace, NormedAddGroup, and NormedAddCommGroup for DirectLimit#39673drocta wants to merge 36 commits into
drocta wants to merge 36 commits into
Commits
Commits on May 19, 2026
- committed
- committed
- committed
- committed
- committed
- committed
Commits on May 20, 2026
in Topology/MetricSpace/DirectLimit , shorten proofs of dist_self and eq_of_dist_eq_zero in instance
committed- committed
- committed
Commits on May 21, 2026
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
remove example showing that DirectLimit.NormedAddGroup.norm_def works for NormedAddCommGroup as well
committed- committed
- committed
Commits on May 22, 2026
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed