Invariant measures of a scalar multiplication

General facts about SMulInvariantMeasure, Mathlib's class of measures invariant under a scalar multiplication, that do not concern ergodicity: the restriction of an invariant measure to an exactly invariant measurable set is again invariant (SMulInvariantMeasure.restrict).

theorem MeasureTheory.SMulInvariantMeasure.restrict {G : Type u_1} {X : Type u_2} [SMul G X] {m : MeasurableSpace X} {μ : Measure X} [MeasurableConstSMul G X] [SMulInvariantMeasure G X μ] {u : Set X} (hum : MeasurableSet u) (huinv : ∀ (g : G), (fun (x : X) => g • x) ⁻¹' u = u) : SMulInvariantMeasure G X (μ.restrict u)

The restriction of an invariant measure to an exactly invariant measurable set is invariant.