Volume/Measure of smul set

Stream: Is there code for X?

[Gareth Ma]

Is there code for the following?

theorem EuclideanSpace.volume_smul {ι : Type*} [Nonempty ι] [Fintype ι]
    {s : Set (EuclideanSpace ℝ ι)} {c : ℝ} :
      volume (c • s) = ENNReal.ofReal ‖c‖ ^ Fintype.card ι * volume s := by
  sorry

If not, how should I approach proving this? I am not too familiar with proving stuff about measures. In fact, I'm not familiar with measure theory Thanks in advance

[Eric Wieser]

I think we have this somewhere

[Eric Wieser]

docs#MeasureTheory.Measure.addHaar_smul_of_nonneg ?

[Eric Wieser]

@loogle (_ : MeasureTheory.Measure _) (_ • _)

[loogle]

:search: MeasureTheory.measure_smul, MeasureTheory.measure_smul_null, and 9 more

[Gareth Ma]

Oops sorry I completely missed this, let me have a look

[Gareth Ma]

Yes perfect, thanks!

[Gareth Ma]

I kept looking for volume.+smul