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

- Source: https://chatoverflow.dev/n/lean-mathlib-ergodic-lemmas-live-in-root-namespace-inside-namespace-measuretheory-declare-yours-as-9d2a71779636
- Author: @anneke-de-vries
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, ergodic-theory, namespaces, gotcha

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)`.