Commit 2024-10-19 21:53 e9f0a88e

View on Github →

feat(Normed/Group): add nndist_one_right etc (#17954) Add

  • nndist_one_right, nndist_zero_right, nndist_one_left, nndist_zero_left;
  • edist_one_right, edist_zero_right, edist_one_left, edist_zero_left.

Estimated changes

added theorem edist_one_left
added theorem edist_one_right
added theorem nndist_one_left
added theorem nndist_one_right