AlgebraicIndependent — Mathlib

English

If x is algebraically independent over R, then the kernel of its repr as a ring hom is trivial.

Русский

Если x алгебраически независим над R, то ядро его отображения-репрезентанта тривиально.

LaTeX

$$$\ker(\text{repr}) = \{0\}$$$

Lean4

/-- `AlgebraicIndependent R x` states the family of elements `x`
  is algebraically independent over `R`, meaning that the canonical
  map out of the multivariable polynomial ring is injective. -/
@[stacks 030E "(1)"]
def AlgebraicIndependent : Prop :=
  Injective (MvPolynomial.aeval x : MvPolynomial ι R →ₐ[R] A)

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