# 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] [comm_ring A] [ A] :
A → Prop

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

Equations
def subalgebra.is_algebraic {R : Type u} {A : Type v} [comm_ring R] [comm_ring A] [ A] :
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] [comm_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] [comm_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] [comm_ring A] [ A] :

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

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

An integral element of an algebra is algebraic.

theorem is_algebraic_iff_is_integral (K : Type u) {A : Type v} [field K] [comm_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 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] :

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_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} :
z(∀ (x : R), S) x = 0x = 0)(∃ (x y : S)) (H : y 0), z * y = x)