algebraMap_injective — Mathlib

English

If AlgebraicIndependent x holds, then the ground ring map algebraMap R A is injective.

Русский

Если x алгебраически независим, то отображение алгебраMap R A инъективно.

LaTeX

$$$\\\\mathrm{algebraMap}(R,A) \\\\text{ is injective }$$$

Lean4

theorem algebraMap_injective : Injective (algebraMap R A) := by
  simpa [Function.comp_def] using
    (Injective.of_comp_iff (algebraicIndependent_iff_injective_aeval.1 hx) MvPolynomial.C).2
      (MvPolynomial.C_injective _ _)

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