Introduction and goal

When this project started, I had thought that the existence of Frobenius elements was specific to the theory of local and global fields, and a slightly more general result held for Dedekind domains. Then Joel Riou pointed out on the Lean Zulip an extremely general result from from Bourbaki's Commutative Algebra (Chapter V, Section 2, number 2, theorem 2, part (ii)). This beautiful result is surely what we want to see in mathlib. Before we state Bourbaki's theorem, let us set the scene.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.