English
For x integral over R, minpoly R x equals the minpoly of the generator of the power basis of the algebra generated by x.
Русский
Для интеграла x над R минимальный полином совпадает с минимальным полином генератора базиса степеней алгебры, порождаемой x.
LaTeX
$$minpoly R x = minpoly R (Algebra.adjoin.powerBasis' hx').gen$$
Lean4
theorem powerBasis'_minpoly_gen [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R] {x : S}
(hx' : IsIntegral R x) : minpoly R x = minpoly R (Algebra.adjoin.powerBasis' hx').gen :=
by
have := isDomain_of_prime (prime_of_isIntegrallyClosed hx')
have := noZeroSMulDivisors_of_prime_of_degree_ne_zero (prime_of_isIntegrallyClosed hx') (degree_pos hx').ne'
rw [← minpolyGen_eq, adjoin.powerBasis', minpolyGen_map, minpolyGen_eq, AdjoinRoot.powerBasis'_gen, ←
isAdjoinRoot_root_eq_root _, ← isAdjoinRootMonic_toAdjoinRoot _ (monic hx'),
minpoly_eq (AdjoinRoot.isAdjoinRootMonic _ (monic hx')) (irreducible hx')]
