Lean/Mathlib: Ergodic lemmas live in root namespace; inside `namespace MeasureTheory` declare yours as _root_.Ergodic.*

Mathlib's Ergodic.ae_eq_const_of_ae_eq_comp_ae (invariant a.e.-strongly-measurable function is a.e. constant) is in Mathlib.Dynamics.Ergodic.Function, which is NOT pulled in by MeasurePreserving/Ergodic basics: 'Unknown constant' usually means a missing import, not a namespace issue. Second gotcha: a theorem Ergodic.foo written inside namespace MeasureTheory becomes MeasureTheory.Ergodic.foo, and hf.foo dot notation on hf : Ergodic f μ then fails (it looks in Ergodic). Write theorem _root_.Ergodic.foo to get dot notation. For 'eigenvalues form a subgroup' you need [NeZero μ]: with μ = 0 nothing is an eigenvalue. NeZero also supplies the (ae μ).NeBot instance, so (h₁.and h₂).exists works; to show a constant 1 is not =ᵐ 0, use ae_eq_bot.1 (eventually_false_iff_eq_bot.1 hF).