Formalization of the Existence of Frobenius Elements
摘要
We use Lean 4 to formalize a proof of the existence of Frobenius elements for finite Galois extensions of number fields.