The normalized angular primitive reverses joint reflection parity.

theorem EulerAngleMeanZeroPrimitive.primitive_neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (P : ℝ) (f : ℝ → E) : (primitive P fun (θ : ℝ) => -f θ) = fun (θ : ℝ) => -primitive P f θ

theorem EulerAngleMeanZeroPrimitive.primitive_reflection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (P : ℝ) (hP : P ≠ 0) (f : ℝ → E) (hf : Continuous f) (hper : Function.Periodic f P) (hmean : ∫ (θ : ℝ) in 0..P, f θ = 0) : (primitive P fun (θ : ℝ) => -f (-θ)) = fun (θ : ℝ) => primitive P f (-θ)

Reflection of the argument contributes one minus sign to a primitive.