Theorems · Definition · field theory

Algebra.trdeg

(R : Type u_2) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Cardinal.{v}

The transcendence degree of a commutative algebra A over a commutative ring R is defined to be the maximal cardinality of an R-algebraically independent set in A.

Defined in

Mathlib.RingTheory.AlgebraicIndependent.Basic

Cited by

39 results in Mathlib

Foundations

Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra