algebraMap_eq_one_iff — Mathlib

English

The equation ι_R x = algebraMap_R (TensorAlgebra) r holds if and only if x = 0 and r = 0.

Русский

Уравнение ι_R x = algebraMap_R r имеет решение только тогда, когда x = 0 и r = 0.

LaTeX

$$$\\iota_R x = \\mathrm{algebraMap}_R( r ) \\iff x = 0 \\wedge r = 0$$$

Lean4

@[simp]
theorem algebraMap_eq_one_iff (x : R) : algebraMap R (TensorAlgebra R M) x = 1 ↔ x = 1 :=
  map_eq_one_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

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