X_injective — Mathlib

English

If R is nontrivial, the map X : σ → MvPolynomial σ R is injective.

Русский

Если R не тривиальна, отображение X: σ → MvPolynomial σ R инъективно.

LaTeX

$$$ [Nontrivial\; R] \Rightarrow Function.Injective (X : σ \to MvPolynomial\; σ\; R)$$$

Lean4

theorem X_injective [Nontrivial R] : Function.Injective (X : σ → MvPolynomial σ R) :=
  (monomial_left_injective one_ne_zero).comp (Finsupp.single_left_injective one_ne_zero)

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