algebraMap_inj — Mathlib

English

The map ι_R: M → TensorAlgebra R M is injective; equivalently, ι_R x = ι_R y implies x = y.

Русский

Карта ι_R: M → TensorAlgebra R M инъективна; то есть ι_R x = ι_R y ⇒ x = y.

LaTeX

$$$\\iota_R x = \\iota_R y \\Rightarrow x = y\\qquad(\\iota_R : M \\to \\mathrm{TensorAlgebra}_R(M))$$$

Lean4

@[simp]
theorem algebraMap_inj (x y : R) : algebraMap R (TensorAlgebra R M) x = algebraMap R (TensorAlgebra R M) y ↔ x = y :=
  (algebraMap_leftInverse M).injective.eq_iff

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