algebraMap_inj — Mathlib

English

The canonical algebra map from R into ExteriorAlgebra R M is injective; equivalently, algebraMap x = algebraMap y implies x = y.

Русский

Каноническое вложение R в ExteriorAlgebra R M инъективно; эквивалентно тому, что algebraMap x = algebraMap y приводит к x = y.

LaTeX

$$$\text{algebraMap}_{R \to \mathrm{ExteriorAlgebra}}(x) = \text{algebraMap}_{R \to \mathrm{ExteriorAlgebra}}(y) \iff x = y$$$

Lean4

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

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