arithFrobAt — Mathlib

English

If Q and Q' lie over the same prime of R, then their arithmetic Frobenius elements arithFrobAt are conjugate in G.

Русский

Если Q и Q' лежат над одним простым в R, то соответствующие арифметические Фробениусы arithFrobAt сопряжены в G.

LaTeX

$$$ IsConj\ (arithFrobAt\; R\; G\; Q)\ (arithFrobAt\; R\; G\; Q').$$$

Lean4

protected theorem arithFrobAt [Q.IsPrime] [Finite (S ⧸ Q)] : IsArithFrobAt R (arithFrobAt R G Q) Q :=
  (exists_primesOver_isConj S G (Q.under R) ⟨⟨Q, ‹_›, ⟨rfl⟩⟩, ‹Finite (S ⧸ Q)›⟩).choose_spec.1 ⟨Q, ‹_›, ⟨rfl⟩⟩

Похожие утверждения