Additive Haar nullness from Hausdorff dimension

A set of Hausdorff dimension below the dimension of its ambient finite-dimensional real normed space is null for every normalization of additive Haar measure.

theorem MeasureTheory.addHaar_eq_zero_of_dimH_lt_finrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E) [μ.IsAddHaarMeasure] {s : Set E} (hs : dimH s < ↑(Module.finrank ℝ E)) : μ s = 0

A set of smaller Hausdorff dimension than its ambient real normed space is null for every additive Haar measure.