Theorems · Definition · field theory

IsAlgebraic

(R : Type u) → {A : Type v} → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → A → Prop

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

Defined in

Mathlib.RingTheory.Algebraic.Defs

Cited by

163 results in Mathlib

Foundations

Depth 110 from the axioms, rests on 2,024 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra