∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S},
  φ.IsArithFrobAt Q → ∀ [IsDomain S] {ζ : S} {m : ℕ}, ζ ^ m = 1 → ↑m ∉ Q → φ ζ = ζ ^ Nat.card (R ⧸ Ideal.under R Q)