Theorems · Theorem · dynamical systems

Ergodic.smul_measure

∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : MeasureTheory.Measure α} {R : Type u_2}
  [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal], Ergodic f μ → ∀ (c : R), Ergodic f (c • μ)

Defined in

Mathlib.Dynamics.Ergodic.Ergodic

Cited by

0 results in Mathlib

Foundations

Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SMulIsScalarTower