`Lnorm0`

[affeldt-aist]

analysis/theories/hoelder.v

Line 86 in c5ea0ab

Lemma Lnorm0 p : p != 0 -> 'N_p[cst 0] = 0.

Try to change this lemma to have no condition when enabling (mu (f @^-1` (setT `\ 0%R))) when p = 0 (which looks like a saner convention than the current one).

@CohenCyril @proux01 @hoheinzollern @t6s