1 Introduction

This blueprint describes the formalization of Lemmas 3.1 and 3.2 from [ 1 ] , which concern monogenic extensions of local rings. The main results are:

• Lemma 3.2 (the étale case): A finite injective étale map of local rings is monogenic, and the minimal polynomial has unit derivative.

• Lemma 3.1 (the partially étale case): If a finite map of local rings admits an étale quotient through a height-one prime, the extension is monogenic.

• Converse: A monogenic extension with unit derivative is étale (i.e., standard étale).

The formalization builds on Mathlib’s theory of étale ring homomorphisms, local rings, residue fields, and the primitive element theorem.

1

B. Viray et al., Monogenic extensions of local rings, arXiv:2503.07846v2, 2025.