English
If p^n • z ∈ adjoin { B.gen } with Eisenstein at minpoly, then z ∈ adjoin { B.gen }. Induct on n.
Русский
Если p^n • z ∈ adjoin { B.gen } и минполином Эйзенштейна, тогда z ∈ adjoin { B.gen }. Индукция по n.
LaTeX
$$$\\text{mem\\_adjoin\\_of\\_smul\\_prime\\_pow\\_smul\\_of\\_minpoly\\_isEisensteinAt}$$$
Lean4
/-- Let `K` be the field of fraction of an integrally closed domain `R` and let `L` be an extension
of `K`, generated by an integral power basis `B` such that the minimal polynomial of `B.gen` is
Eisenstein at `p`. Given `z : L` integral over `R`, if `p ^ n • z ∈ adjoin R {B.gen}`, then
`z ∈ adjoin R {B.gen}`. Together with `Algebra.discr_mul_isIntegral_mem_adjoin` this result often
allows to compute the ring of integers of `L`. -/
theorem mem_adjoin_of_smul_prime_pow_smul_of_minpoly_isEisensteinAt {B : PowerBasis K L} (hp : Prime p)
(hBint : IsIntegral R B.gen) {n : ℕ} {z : L} (hzint : IsIntegral R z)
(hz : p ^ n • z ∈ adjoin R ({ B.gen } : Set L)) (hei : (minpoly R B.gen).IsEisensteinAt 𝓟) :
z ∈ adjoin R ({ B.gen } : Set L) := by
induction n with
| zero => simpa using hz
| succ n hn =>
rw [_root_.pow_succ', mul_smul] at hz
exact hn (mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt hp hBint (hzint.smul _) hz hei)
