Ergodicity of an irrational rotation

In this file we prove that rotation of AddCircle p by a is ergodic if and only if a has infinite order (in other words, if a / p is irrational).

theorem AddCircle.ergodic_add_left {p : ℝ} [Fact (0 < p)] {a : AddCircle p} : Ergodic (fun (x : AddCircle p) => a + x) MeasureTheory.volume ↔ addOrderOf a = 0

theorem AddCircle.ergodic_add_right {p : ℝ} [Fact (0 < p)] {a : AddCircle p} : Ergodic (fun (x : AddCircle p) => x + a) MeasureTheory.volume ↔ addOrderOf a = 0