algebraicIndependent_iff_ker_eq_bot

English

The transcendence degree trdeg(R,A) is defined as the supremum of the cardinalities of R-algebraically independent subsets of A.

Русский

Степень трансцендентности trdeg(R,A) определяется как наибольшая мощность множества R-алгебраически независимых подмножеств A.

LaTeX

$$$\\\\operatorname{trdeg}(R,A) = \\sup_{\\iota} \\{ \\#\\iota \\\\mid \\text{AlgebraicIndependent}(R,\\iota \\to A)\\}$$$

Lean4

theorem algebraicIndependent_iff_ker_eq_bot :
    AlgebraicIndependent R x ↔ RingHom.ker (MvPolynomial.aeval x : MvPolynomial ι R →ₐ[R] A).toRingHom = ⊥ :=
  RingHom.injective_iff_ker_eq_bot _

Похожие утверждения