Vanishing order under a root-of-unity rotation

For an analytic germ f and a primitive Nth root of unity ζ, the difference f (ζ * t) - f t detects every nonconstant term of degree less than N. Thus its order, capped at N, equals the capped order of f t - f 0. This converts contacts of ramified root branches with their central values into contacts between branches permuted by rotation.

theorem AnalyticAt.min_analyticOrderAt_comp_mul_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f 0) {N : ℕ} {ζ : 𝕜} (hζ : IsPrimitiveRoot ζ N) : min (↑N) (analyticOrderAt (fun (t : 𝕜) => f (ζ * t) - f t) 0) = min (↑N) (analyticOrderAt (fun (t : 𝕜) => f t - f 0) 0)

Rotation by a primitive Nth root detects the first nonconstant term below degree N. The equality remains valid for a constant germ and for contact order at least N.