algebraMap_eq_one_iff — Mathlib

English

An element x ∈ R maps to the identity 1 in the symmetric algebra if and only if x = 1.

Русский

Элемент x ∈ R отображается в единицу в симметрической алгебре тогда и только тогда, когда x = 1.

LaTeX

$$$\operatorname{algebraMap}_R(x) = 1 \iff x = 1$$$

Lean4

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

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