injective — Mathlib

English

If the base ring R is nontrivial, the map i ↦ b_i sending indices to basis vectors is injective; in particular, distinct indices give distinct basis vectors.

Русский

Если кольцо R не тривиально, отображение i ↦ b_i из индексов в базисные векторы инъективно; то есть разные индексы дают разные базисные векторы.

LaTeX

$$$\text{If } \mathbf{1}_R \neq 0,\text{ then } i \mapsto b_i\text{ is injective.}$$$

Lean4

protected theorem injective [Nontrivial R] : Injective b :=
  b.repr.symm.injective.comp fun _ _ => (Finsupp.single_left_inj (one_ne_zero : (1 : R) ≠ 0)).mp

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