Theorems · Inductive type · field theory

Algebra.IsAlgebraic

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

An algebra is algebraic if all its elements are algebraic.

Defined in

Mathlib.RingTheory.Algebraic.Defs

Cited by

322 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 21 definitions · uses no axioms

Assumes

CommRingRingAlgebra