# mathlib3documentation

field_theory.minpoly.is_integrally_closed

# Minimal polynomials over a GCD monoid #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file specializes the theory of minpoly to the case of an algebra over a GCD monoid.

## Main results #

• is_integrally_closed_eq_field_fractions: For integrally closed domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field.

• is_integrally_closed_dvd : For integrally closed domains, the minimal polynomial divides any primitive polynomial that has the integral element as root.

• is_integrally_closed_unique : The minimal polynomial of an element x is uniquely characterized by its defining property: if there is another monic polynomial of minimal degree that has x as a root, then this polynomial is equal to the minimal polynomial of x.

theorem minpoly.is_integrally_closed_eq_field_fractions {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] (K : Type u_3) (L : Type u_4) [field K] [ K] [ K] [field L] [ L] [ L] [ L] [ L] [ L] [is_domain S] {s : S} (hs : s) :
( L) s) = (minpoly R s)

For integrally closed domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field. See minpoly.is_integrally_closed_eq_field_fractions' if S is already a K-algebra.

theorem minpoly.is_integrally_closed_eq_field_fractions' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] (K : Type u_3) [field K] [ K] [ K] [is_domain S] [ S] [ S] {s : S} (hs : s) :
s = (minpoly R s)

For integrally closed domains, the minimal polynomial over the ring is the same as the minimal polynomial over the fraction field. Compared to minpoly.is_integrally_closed_eq_field_fractions, this version is useful if the element is in a ring that is already a K-algebra.

theorem minpoly.is_integrally_closed_dvd {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] [nontrivial R] {s : S} (hs : s) {p : polynomial R} (hp : p = 0) :
s p

For integrally closed rings, the minimal polynomial divides any polynomial that has the integral element as root. See also minpoly.dvd which relaxes the assumptions on S in exchange for stronger assumptions on R.

theorem minpoly.is_integrally_closed_dvd_iff {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] [nontrivial R] {s : S} (hs : s) (p : polynomial R) :
p = 0 s p
theorem minpoly.ker_eval {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {s : S} (hs : s) :
theorem minpoly.is_integrally_closed.degree_le_of_ne_zero {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {s : S} (hs : s) {p : polynomial R} (hp0 : p 0) (hp : p = 0) :

If an element x is a root of a nonzero polynomial p, then the degree of p is at least the degree of the minimal polynomial of x. See also minpoly.degree_le_of_ne_zero which relaxes the assumptions on S in exchange for stronger assumptions on R.

theorem minpoly.is_integrally_closed.minpoly.unique {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {s : S} {P : polynomial R} (hmo : P.monic) (hP : P = 0) (Pmin : (Q : , Q.monic Q = 0 P.degree Q.degree) :
P = s

The minimal polynomial of an element x is uniquely characterized by its defining property: if there is another monic polynomial of minimal degree that has x as a root, then this polynomial is equal to the minimal polynomial of x. See also minpoly.unique which relaxes the assumptions on S in exchange for stronger assumptions on R.

theorem minpoly.prime_of_is_integrally_closed {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (hx : x) :
theorem minpoly.to_adjoin.injective {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (hx : x) :
@[simp]
theorem minpoly.equiv_adjoin_symm_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (hx : x) (ᾰ : {x})) :
noncomputable def minpoly.equiv_adjoin {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (hx : x) :

The algebra isomorphism adjoin_root (minpoly R x) ≃ₐ[R] adjoin R x

Equations
@[simp]
theorem minpoly.equiv_adjoin_apply {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (hx : x) (ᾰ : adjoin_root (minpoly R x)) :
= (adjoin_root.lift {x})) x, _⟩ _)
@[simp]
theorem algebra.adjoin.power_basis'_dim {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (hx : x) :
@[simp]
theorem algebra.adjoin.power_basis'_gen {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (hx : x) :
= x, _⟩
noncomputable def algebra.adjoin.power_basis' {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (hx : x) :
{x})

The power_basis of adjoin R {x} given by x. See algebra.adjoin.power_basis for a version over a field.

Equations
@[simp]
theorem power_basis.of_gen_mem_adjoin'_gen {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [is_domain R] [ S] [is_domain S] {x : S} (B : S) (hint : x) (hx : B.gen {x}) :
The power basis given by x if B.gen ∈ adjoin R {x}.