algebraMap_injective — Mathlib

English

The embedding of K[X] into RatFunc K is injective; i.e., distinct polynomials map to distinct elements of RatFunc K.

Русский

Встраивание K[X] в RatFunc K инъективно; различные многочлены отображаются в разные элементы RatFunc K.

LaTeX

$$$\text{Injective}(\text{algebraMap } K[X] \to \text{RatFunc } K)$$$

Lean4

theorem algebraMap_injective : Function.Injective (algebraMap K[X] (RatFunc K)) :=
  by
  rw [← ofFractionRing_comp_algebraMap]
  exact ofFractionRing_injective.comp (IsFractionRing.injective _ _)

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