English
The Frobenius element arithFrobAt is a Frobenius at the chosen prime Q: its associated IsArithFrobAt relation holds.
Русский
Фробениус-элемент arithFrobAt является Фробениусом над выбранным простым Q: выполняется соответствующее отношение IsArithFrobAt.
LaTeX
$$$ IsArithFrobAt\; R\ (arithFrobAt\; R\ G\ Q)\ Q.$$$
Lean4
/-- Let `G` be a finite group acting on `S`, `R` be the fixed subring, and `Q` be a prime of `S`
with finite residue field. This is an arbitrary choice of a Frobenius over `Q`. It is chosen so that
the Frobenius elements of `Q₁` and `Q₂` are conjugate if they lie over the same prime. -/
noncomputable def _root_.arithFrobAt [Q.IsPrime] [Finite (S ⧸ Q)] : G :=
(exists_primesOver_isConj S G (Q.under R) ⟨⟨Q, ‹_›, ⟨rfl⟩⟩, ‹Finite (S ⧸ Q)›⟩).choose ⟨Q, ‹_›, ⟨rfl⟩⟩
