The volume measures on ℤₚ and ℚₚ

[YaelDillies]

For $p$ a prime, the Haar measure on $\mathbb{Q}_p$ making (the copy of) $\mathbb{Z}_p$ (inside $\mathbb Q_p$) have measure $1$ extends the Haar measure on $\mathbb Z_p$ with total mass $1$.

This sorry will appear in FLT/HaarMeasure/MeasurableSpacePadics.lean once #223 is merged.