Commit 2023-11-09 12:07 4055c8b4

feat: change definition for p = 0 in piLp (#8290) The current definition of the distance in piLp uses the distance for p > 0, but avoids it for p = 0. We change the definition for p = 0 to also have it in terms of the distance, to make sure it is reasonable even when one uses non-Hausdorff spaces.This matches what has been done for prodLp in #6136.