# mathlibdocumentation

ring_theory.algebraic

# Algebraic elements and algebraic extensions #

An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial. An R-algebra is algebraic over R if and only if all its elements are algebraic over R. The main result in this file proves transitivity of algebraicity: a tower of algebraic field extensions is algebraic.

def is_algebraic (R : Type u) {A : Type v} [comm_ring R] [ring A] [ A] (x : A) :
Prop

An element of an R-algebra is algebraic over R if it is the root of a nonzero polynomial.

Equations
def transcendental (R : Type u) {A : Type v} [comm_ring R] [ring A] [ A] (x : A) :
Prop

An element of an R-algebra is transcendental over R if it is not algebraic over R.

Equations
def subalgebra.is_algebraic {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : A) :
Prop

A subalgebra is algebraic if all its elements are algebraic.

Equations
def algebra.is_algebraic (R : Type u) (A : Type v) [comm_ring R] [ring A] [ A] :
Prop

An algebra is algebraic if all its elements are algebraic.

Equations
• = ∀ (x : A), x
theorem subalgebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] (S : A) :

A subalgebra is algebraic if and only if it is algebraic an algebra.

theorem algebra.is_algebraic_iff {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] :

An algebra is algebraic if and only if it is algebraic as a subalgebra.

theorem is_algebraic_iff_not_injective {R : Type u} {A : Type v} [comm_ring R] [ring A] [ A] {x : A} :
theorem is_integral.is_algebraic (R : Type u) {A : Type v} [comm_ring R] [nontrivial R] [ring A] [ A] {x : A} (h : x) :
x

An integral element of an algebra is algebraic.

theorem is_algebraic_algebra_map {R : Type u} {A : Type v} [comm_ring R] [nontrivial R] [ring A] [ A] (a : R) :
( A) a)

An element of R is algebraic, when viewed as an element of the R-algebra A.

theorem is_algebraic_iff_is_integral (K : Type u) {A : Type v} [field K] [ring A] [ A] {x : A} :
x x

An element of an algebra over a field is algebraic if and only if it is integral.

theorem is_algebraic_iff_is_integral' (K : Type u) {A : Type v} [field K] [ring A] [ A] :
theorem algebra.is_algebraic_trans {K : Type u_1} {L : Type u_2} {A : Type u_3} [field K] [field L] [comm_ring A] [ L] [ A] [ A] [ A] (L_alg : L) (A_alg : A) :

If L is an algebraic field extension of K and A is an algebraic algebra over L, then A is algebraic over K.

theorem algebra.is_algebraic_of_larger_base (K : Type u_1) (L : Type u_2) {A : Type u_3} [field K] [field L] [comm_ring A] [ L] [ A] [ A] [ A] (A_alg : A) :

If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K

theorem algebra.is_algebraic_of_finite {K : Type u_1} {L : Type u_2} [field K] [field L] [ L] [finite : L] :

A field extension is algebraic if it is finite.

theorem exists_integral_multiple {R : Type u_1} {S : Type u_2} [comm_ring S] [ S] {z : S} (hz : z) (inj : ∀ (x : R), S) x = 0x = 0) :
∃ (x : S)) (y : R) (H : y 0), z * S) y = x
theorem is_integral_closure.exists_smul_eq_mul {R : Type u_1} {S : Type u_2} [comm_ring S] {L : Type u_3} [field L] [ S] [ L] [ L] [ L] [ L] (h : L) (inj : function.injective L)) (a : S) {b : S} (hb : b 0) :
∃ (c : S) (d : R) (H : d 0), d a = b * c

A fraction (a : S) / (b : S) can be reduced to (c : S) / (d : R), if S is the integral closure of R in an algebraic extension L of R.

theorem inv_eq_of_aeval_div_X_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] {x : L} {p : polynomial K} (aeval_ne : p.div_X 0) :
x⁻¹ = p.div_X / ( p - L) (p.coeff 0))
theorem inv_eq_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] {x : L} {p : polynomial K} (aeval_eq : p = 0) (coeff_zero_ne : p.coeff 0 0) :
x⁻¹ = -( p.div_X / L) (p.coeff 0))
theorem subalgebra.inv_mem_of_root_of_coeff_zero_ne_zero {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] (A : L) {x : A} {p : polynomial K} (aeval_eq : p = 0) (coeff_zero_ne : p.coeff 0 0) :
theorem subalgebra.inv_mem_of_algebraic {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] (A : L) {x : A} (hx : x) :
theorem subalgebra.is_field_of_algebraic {K : Type u_3} {L : Type u_4} [field K] [field L] [ L] (A : L) (hKL : L) :

In an algebraic extension L/K, an intermediate subalgebra is a field.