English
AlgebraicIndependent R x is equivalent to the kernel of the evaluation map from a polynomial ring being trivial; i.e., the kernel equals ⊥.
Русский
Алгебраическая независимость над R для x эквивалентна тривиальности ядра отображения оценки; ядро равно ⊥.
LaTeX
$$$\\\\mathrm{AlgebraicIndependent}(R,x) \\\\iff \\\\ker( MvPolynomial.aeval\_x : MvPolynomial ι R \\\\to A ).toRingHom = \\perp$$$
Lean4
/-- 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`. -/
@[stacks 030G]
def trdeg : Cardinal.{v} :=
⨆ ι : { s : Set A // AlgebraicIndepOn R _root_.id s }, Cardinal.mk ι.1
