Null traces of absolutely continuous curves

An absolutely continuous curve in a finite-dimensional real normed space of dimension greater than one has an additive-Haar-null trace.

theorem AbsolutelyContinuousOnInterval.addHaar_image_uIcc_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {γ : ℝ → E} {a b : ℝ} (hγ : AbsolutelyContinuousOnInterval γ a b) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hd : 1 < Module.finrank ℝ E) : μ (γ '' Set.uIcc a b) = 0

The trace of an absolutely continuous curve is additive-Haar-null in ambient dimension greater than one.