algebraMap_eq_zero_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem algebraMap_eq_zero_iff (x : R) : algebraMap R (SymmetricAlgebra R M) x = 0 ↔ x = 0 :=
  map_eq_zero_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

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