algebraicIndependent_iff_injective_aeval

English

For a family x, AlgebraicIndependent R x holds if and only if the algebra homomorphism aeval x : MvPolynomial ι R → A is injective.

Русский

Для семейства x алгебраическая независимость над R эквивалентна инъективности гомоморфизма aeval x: MvPolynomial ι R → A.

LaTeX

$$$\\text{AlgebraicIndependent } R\\, x \\;\\iff\\; \\text{Injective } (\\mathrm{MvPolynomial}.aeval\\, x : \\mathrm{MvPolynomial}\\, ι\\, R \\to_A A)$$$

Lean4

theorem algebraicIndependent_iff_injective_aeval :
    AlgebraicIndependent R x ↔ Injective (MvPolynomial.aeval x : MvPolynomial ι R →ₐ[R] A) :=
  Iff.rfl

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